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

Metamath Proof Explorer

Theorem dfssf

Description: Equivalence for subclass relation, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 3-Jul-1994) (Revised by Andrew Salmon, 27-Aug-2011) Avoid ax-13 . (Revised by GG, 19-May-2023)

Ref Expression
Hypotheses dfssf.1 
|- F/_ x A
dfssf.2 
|- F/_ x B
Assertion dfssf 
|- ( A C_ B <-> A. x ( x e. A -> x e. B ) )

Proof

Step Hyp Ref Expression
1 dfssf.1 
 |-  F/_ x A
2 dfssf.2 
 |-  F/_ x B
3 df-ss 
 |-  ( A C_ B <-> A. z ( z e. A -> z e. B ) )
4 1 nfcri 
 |-  F/ x z e. A
5 2 nfcri 
 |-  F/ x z e. B
6 4 5 nfim 
 |-  F/ x ( z e. A -> z e. B )
7 nfv 
 |-  F/ z ( x e. A -> x e. B )
8 eleq1w 
 |-  ( z = x -> ( z e. A <-> x e. A ) )
9 eleq1w 
 |-  ( z = x -> ( z e. B <-> x e. B ) )
10 8 9 imbi12d 
 |-  ( z = x -> ( ( z e. A -> z e. B ) <-> ( x e. A -> x e. B ) ) )
11 6 7 10 cbvalv1 
 |-  ( A. z ( z e. A -> z e. B ) <-> A. x ( x e. A -> x e. B ) )
12 3 11 bitri 
 |-  ( A C_ B <-> A. x ( x e. A -> x e. B ) )