This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fabexgOLD

Description: Obsolete version of fabexg as of 9-Jun-2025. (Contributed by Paul Chapman, 25-Feb-2008) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis fabexg.1 ⊢ 𝐹 = { 𝑥 ∣ ( 𝑥 : 𝐴 ⟶ 𝐵 ∧ 𝜑 ) }
Assertion fabexgOLD ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → 𝐹 ∈ V )

Proof

Step Hyp Ref Expression
1 fabexg.1 ⊢ 𝐹 = { 𝑥 ∣ ( 𝑥 : 𝐴 ⟶ 𝐵 ∧ 𝜑 ) }
2 xpexg ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 𝐴 × 𝐵 ) ∈ V )
3 pwexg ⊢ ( ( 𝐴 × 𝐵 ) ∈ V → 𝒫 ( 𝐴 × 𝐵 ) ∈ V )
4 fssxp ⊢ ( 𝑥 : 𝐴 ⟶ 𝐵 → 𝑥 ⊆ ( 𝐴 × 𝐵 ) )
5 velpw ⊢ ( 𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) ↔ 𝑥 ⊆ ( 𝐴 × 𝐵 ) )
6 4 5 sylibr ⊢ ( 𝑥 : 𝐴 ⟶ 𝐵 → 𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) )
7 6 anim1i ⊢ ( ( 𝑥 : 𝐴 ⟶ 𝐵 ∧ 𝜑 ) → ( 𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝜑 ) )
8 7 ss2abi ⊢ { 𝑥 ∣ ( 𝑥 : 𝐴 ⟶ 𝐵 ∧ 𝜑 ) } ⊆ { 𝑥 ∣ ( 𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝜑 ) }
9 1 8 eqsstri ⊢ 𝐹 ⊆ { 𝑥 ∣ ( 𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝜑 ) }
10 ssab2 ⊢ { 𝑥 ∣ ( 𝑥 ∈ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝜑 ) } ⊆ 𝒫 ( 𝐴 × 𝐵 )
11 9 10 sstri ⊢ 𝐹 ⊆ 𝒫 ( 𝐴 × 𝐵 )
12 ssexg ⊢ ( ( 𝐹 ⊆ 𝒫 ( 𝐴 × 𝐵 ) ∧ 𝒫 ( 𝐴 × 𝐵 ) ∈ V ) → 𝐹 ∈ V )
13 11 12 mpan ⊢ ( 𝒫 ( 𝐴 × 𝐵 ) ∈ V → 𝐹 ∈ V )
14 2 3 13 3syl ⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → 𝐹 ∈ V )