Metamath Proof Explorer


Theorem dfss2f

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 Gino Giotto, 19-May-2023)

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

Proof

Step Hyp Ref Expression
1 dfss2f.1
 |-  F/_ x A
2 dfss2f.2
 |-  F/_ x B
3 dfss2
 |-  ( 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 ) )