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	$⊢ F = \{x \| (x : A ⟶ B \land φ)\}$
	Assertion	fabexgOLD	$⊢ (A \in C \land B \in D) \to F \in V$

Proof

Step	Hyp	Ref	Expression
1		fabexg.1	$⊢ F = \{x \| (x : A ⟶ B \land φ)\}$
2		xpexg	$⊢ (A \in C \land B \in D) \to A \times B \in V$
3		pwexg	$⊢ A \times B \in V \to 𝒫 (A \times B) \in V$
4		fssxp	$⊢ x : A ⟶ B \to x \subseteq A \times B$
5		velpw	$⊢ x \in 𝒫 (A \times B) \leftrightarrow x \subseteq A \times B$
6	4 5	sylibr	$⊢ x : A ⟶ B \to x \in 𝒫 (A \times B)$
7	6	anim1i	$⊢ (x : A ⟶ B \land φ) \to (x \in 𝒫 (A \times B) \land φ)$
8	7	ss2abi	$⊢ \{x \| (x : A ⟶ B \land φ)\} \subseteq \{x \| (x \in 𝒫 (A \times B) \land φ)\}$
9	1 8	eqsstri	$⊢ F \subseteq \{x \| (x \in 𝒫 (A \times B) \land φ)\}$
10		ssab2	$⊢ \{x \| (x \in 𝒫 (A \times B) \land φ)\} \subseteq 𝒫 (A \times B)$
11	9 10	sstri	$⊢ F \subseteq 𝒫 (A \times B)$
12		ssexg	$⊢ (F \subseteq 𝒫 (A \times B) \land 𝒫 (A \times B) \in V) \to F \in V$
13	11 12	mpan	$⊢ 𝒫 (A \times B) \in V \to F \in V$
14	2 3 13	3syl	$⊢ (A \in C \land B \in D) \to F \in V$