Theorem dfss3f 3926

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 3925	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4		df-ral 3076	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
5	3, 4	bitr4i 280	1 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵)

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1557   ∈ wcel 2141  Ⅎwnfc 2908  ∀wral 3075   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-11 2190  ax-12 2211

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-nf 1803  df-clel 2836  df-nfc 2910  df-ral 3076  df-ss 3919

This theorem is referenced by:  nfss  3927  nfchnd  18633  sigaclcu2  34377  bnj1498  35316  heibor1  38269  ssrabf  45652  ssrab2f  45655  limsupequzmpt2  46252  liminfequzmpt2  46325  pimconstlt1  47236  pimltpnff  47237  pimdecfgtioc  47249  pimincfltioc  47250  pimdecfgtioo  47251  pimincfltioo  47252  pimgtmnff  47256