Theorem dfss3f 3595

Description: Equivalence for subclass relation, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 20-Mar-2004.)

Hypotheses

Ref	Expression
dfss2f.1	|- F/_ x A
dfss2f.2	|- F/_ x B

Assertion

Ref	Expression
dfss3f	|- ( A C_ B <-> A. x e. A x e. B )

Proof of Theorem dfss3f

Step	Hyp	Ref	Expression
1		dfss2f.1	. . 3 |- F/_ x A
2		dfss2f.2	. . 3 |- F/_ x B
3	1, 2	dfss2f 3594	. 2 |- ( A C_ B <-> A. x ( x e. A -> x e. B ) )
4		df-ral 2917	. 2 |- ( A. x e. A x e. B <-> A. x ( x e. A -> x e. B ) )
5	3, 4	bitr4i 267	1 |- ( A C_ B <-> A. x e. A x e. B )

Syntax hints:   -> wi 4   <-> wb 196   A.wal 1481   e. wcel 1990   F/_wnfc 2751   A.wral 2912   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-in 3581  df-ss 3588

This theorem is referenced by:  nfss  3596  sigaclcu2  30183  bnj1498  31129  heibor1  33609  ssrabf  39298  ssrab2f  39300  limsupequzmpt2  39950  liminfequzmpt2  40023  pimconstlt1  40915  pimltpnf  40916  pimiooltgt  40921  pimdecfgtioc  40925  pimincfltioc  40926  pimdecfgtioo  40927  pimincfltioo  40928  sssmf  40947