Theorem dfss3f 3950

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538   ∈ wcel 2108  Ⅎwnfc 2883  ∀wral 3051   ⊆ wss 3926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-11 2157  ax-12 2177

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784  df-clel 2809  df-nfc 2885  df-ral 3052  df-ss 3943

This theorem is referenced by:  nfss  3951  sigaclcu2  34097  bnj1498  35038  heibor1  37780  ssrabf  45086  ssrab2f  45089  limsupequzmpt2  45695  liminfequzmpt2  45768  pimconstlt1  46679  pimltpnff  46680  pimiooltgt  46687  pimdecfgtioc  46692  pimincfltioc  46693  pimdecfgtioo  46694  pimincfltioo  46695  pimgtmnff  46699  sssmf  46715