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 ( ( 𝐴𝐵 ∧ ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) ) ) → ( 𝐴 ∈ { 𝑥𝜑 } ↔ 𝜓 ) )

Proof

Step Hyp Ref Expression
1 nfcv 𝑥 𝐴
2 nfab1 𝑥 { 𝑥𝜑 }
3 2 nfel2 𝑥 𝐴 ∈ { 𝑥𝜑 }
4 nfv 𝑥 𝜓
5 3 4 nfbi 𝑥 ( 𝐴 ∈ { 𝑥𝜑 } ↔ 𝜓 )
6 pm5.5 ( 𝑥 = 𝐴 → ( ( 𝑥 = 𝐴 → ( 𝐴 ∈ { 𝑥𝜑 } ↔ 𝜓 ) ) ↔ ( 𝐴 ∈ { 𝑥𝜑 } ↔ 𝜓 ) ) )
7 1 5 6 spcgf ( 𝐴𝐵 → ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝐴 ∈ { 𝑥𝜑 } ↔ 𝜓 ) ) → ( 𝐴 ∈ { 𝑥𝜑 } ↔ 𝜓 ) ) )
8 abid ( 𝑥 ∈ { 𝑥𝜑 } ↔ 𝜑 )
9 eleq1 ( 𝑥 = 𝐴 → ( 𝑥 ∈ { 𝑥𝜑 } ↔ 𝐴 ∈ { 𝑥𝜑 } ) )
10 8 9 bitr3id ( 𝑥 = 𝐴 → ( 𝜑𝐴 ∈ { 𝑥𝜑 } ) )
11 10 bibi1d ( 𝑥 = 𝐴 → ( ( 𝜑𝜓 ) ↔ ( 𝐴 ∈ { 𝑥𝜑 } ↔ 𝜓 ) ) )
12 11 biimpd ( 𝑥 = 𝐴 → ( ( 𝜑𝜓 ) → ( 𝐴 ∈ { 𝑥𝜑 } ↔ 𝜓 ) ) )
13 12 a2i ( ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) ) → ( 𝑥 = 𝐴 → ( 𝐴 ∈ { 𝑥𝜑 } ↔ 𝜓 ) ) )
14 13 alimi ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) ) → ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝐴 ∈ { 𝑥𝜑 } ↔ 𝜓 ) ) )
15 7 14 impel ( ( 𝐴𝐵 ∧ ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝜑𝜓 ) ) ) → ( 𝐴 ∈ { 𝑥𝜑 } ↔ 𝜓 ) )