Theorem dfss3f 3923

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568   ∈ wcel 2145  Ⅎwnfc 2907  ∀wral 3076   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-11 2194  ax-12 2213

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817  df-clel 2835  df-nfc 2909  df-ral 3077  df-ss 3916

This theorem is used by:  nfss  3924  nfchnd  18699  sigaclcu2  34630  bnj1498  35570  heibor1  38560  ssrabf  45946  ssrab2f  45949  limsupequzmpt2  46546  liminfequzmpt2  46619  pimconstlt1  47530  pimltpnff  47531  pimdecfgtioc  47543  pimincfltioc  47544  pimdecfgtioo  47545  pimincfltioo  47546  pimgtmnff  47550