Theorem dfss3f 3974

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

Hypotheses

Ref	Expression
dfssf.1	⊢ Ⅎ𝑥𝐴
dfssf.2	⊢ Ⅎ𝑥𝐵

Assertion

Ref	Expression
dfss3f	⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵)

Proof of Theorem dfss3f

Step	Hyp	Ref	Expression
1		dfssf.1	. . 3 ⊢ Ⅎ𝑥𝐴
2		dfssf.2	. . 3 ⊢ Ⅎ𝑥𝐵
3	1, 2	dfssf 3973	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4		df-ral 3061	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
5	3, 4	bitr4i 278	1 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵)

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1537   ∈ wcel 2107  Ⅎwnfc 2889  ∀wral 3060   ⊆ wss 3950

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-11 2156  ax-12 2176

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-nf 1783  df-clel 2815  df-nfc 2891  df-ral 3061  df-ss 3967

This theorem is referenced by:  nfss  3975  sigaclcu2  34122  bnj1498  35076  heibor1  37818  ssrabf  45124  ssrab2f  45127  limsupequzmpt2  45738  liminfequzmpt2  45811  pimconstlt1  46722  pimltpnff  46723  pimiooltgt  46730  pimdecfgtioc  46735  pimincfltioc  46736  pimdecfgtioo  46737  pimincfltioo  46738  pimgtmnff  46742  sssmf  46758