Theorem dfss3f 3790

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	⊢ Ⅎ𝑥𝐴
dfss2f.2	⊢ Ⅎ𝑥𝐵

Assertion

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

Proof of Theorem dfss3f

Step	Hyp	Ref	Expression
1		dfss2f.1	. . 3 ⊢ Ⅎ𝑥𝐴
2		dfss2f.2	. . 3 ⊢ Ⅎ𝑥𝐵
3	1, 2	dfss2f 3789	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4		df-ral 3094	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
5	3, 4	bitr4i 270	1 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑥 ∈ 𝐵)

Syntax hints:   → wi 4   ↔ wb 198  ∀wal 1651   ∈ wcel 2157  Ⅎwnfc 2928  ∀wral 3089   ⊆ wss 3769

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-ral 3094  df-in 3776  df-ss 3783

This theorem is referenced by:  nfss  3791  sigaclcu2  30699  bnj1498  31646  heibor1  34096  ssrabf  40056  ssrab2f  40058  limsupequzmpt2  40694  liminfequzmpt2  40767  pimconstlt1  41661  pimltpnf  41662  pimiooltgt  41667  pimdecfgtioc  41671  pimincfltioc  41672  pimdecfgtioo  41673  pimincfltioo  41674  sssmf  41693