Metamath Proof Explorer


Theorem dfss2OLD

Description: Obsolete version of dfss2 as of 16-May-2024. (Contributed by NM, 8-Jan-2002) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion dfss2OLD ( 𝐴𝐵 ↔ ∀ 𝑥 ( 𝑥𝐴𝑥𝐵 ) )

Proof

Step Hyp Ref Expression
1 dfss ( 𝐴𝐵𝐴 = ( 𝐴𝐵 ) )
2 df-in ( 𝐴𝐵 ) = { 𝑥 ∣ ( 𝑥𝐴𝑥𝐵 ) }
3 2 eqeq2i ( 𝐴 = ( 𝐴𝐵 ) ↔ 𝐴 = { 𝑥 ∣ ( 𝑥𝐴𝑥𝐵 ) } )
4 abeq2 ( 𝐴 = { 𝑥 ∣ ( 𝑥𝐴𝑥𝐵 ) } ↔ ∀ 𝑥 ( 𝑥𝐴 ↔ ( 𝑥𝐴𝑥𝐵 ) ) )
5 1 3 4 3bitri ( 𝐴𝐵 ↔ ∀ 𝑥 ( 𝑥𝐴 ↔ ( 𝑥𝐴𝑥𝐵 ) ) )
6 pm4.71 ( ( 𝑥𝐴𝑥𝐵 ) ↔ ( 𝑥𝐴 ↔ ( 𝑥𝐴𝑥𝐵 ) ) )
7 6 albii ( ∀ 𝑥 ( 𝑥𝐴𝑥𝐵 ) ↔ ∀ 𝑥 ( 𝑥𝐴 ↔ ( 𝑥𝐴𝑥𝐵 ) ) )
8 5 7 bitr4i ( 𝐴𝐵 ↔ ∀ 𝑥 ( 𝑥𝐴𝑥𝐵 ) )