Metamath Proof Explorer

Theorem elabgtOLD

Description: Obsolete version of elabgt as of 12-Oct-2024. (Contributed by NM, 7-Nov-2005) (Proof shortened by Andrew Salmon, 8-Jun-2011) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	elabgtOLD	$⊢ (A \in B \land \forall x (x = A \to (φ \leftrightarrow ψ))) \to (A \in \{x \| φ\} \leftrightarrow ψ)$

Proof

Step	Hyp	Ref	Expression
1		nfcv	$⊢ \underline{Ⅎ} x A$
2		nfab1	$⊢ \underline{Ⅎ} x \{x \| φ\}$
3	2	nfel2	$⊢ Ⅎ x A \in \{x \| φ\}$
4		nfv	$⊢ Ⅎ x ψ$
5	3 4	nfbi	$⊢ Ⅎ x (A \in \{x \| φ\} \leftrightarrow ψ)$
6		pm5.5	$⊢ x = A \to ((x = A \to (A \in \{x \| φ\} \leftrightarrow ψ)) \leftrightarrow (A \in \{x \| φ\} \leftrightarrow ψ))$
7	1 5 6	spcgf	$⊢ A \in B \to (\forall x (x = A \to (A \in \{x \| φ\} \leftrightarrow ψ)) \to (A \in \{x \| φ\} \leftrightarrow ψ))$
8		abid	$⊢ x \in \{x \| φ\} \leftrightarrow φ$
9		eleq1	$⊢ x = A \to (x \in \{x \| φ\} \leftrightarrow A \in \{x \| φ\})$
10	8 9	bitr3id	$⊢ x = A \to (φ \leftrightarrow A \in \{x \| φ\})$
11	10	bibi1d	$⊢ x = A \to ((φ \leftrightarrow ψ) \leftrightarrow (A \in \{x \| φ\} \leftrightarrow ψ))$
12	11	biimpd	$⊢ x = A \to ((φ \leftrightarrow ψ) \to (A \in \{x \| φ\} \leftrightarrow ψ))$
13	12	a2i	$⊢ (x = A \to (φ \leftrightarrow ψ)) \to (x = A \to (A \in \{x \| φ\} \leftrightarrow ψ))$
14	13	alimi	$⊢ \forall x (x = A \to (φ \leftrightarrow ψ)) \to \forall x (x = A \to (A \in \{x \| φ\} \leftrightarrow ψ))$
15	7 14	impel	$⊢ (A \in B \land \forall x (x = A \to (φ \leftrightarrow ψ))) \to (A \in \{x \| φ\} \leftrightarrow ψ)$