Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfss3f Structured version   Visualization version   GIF version

Theorem dfss3f 3885
 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
StepHypRef Expression
1 dfss2f.1 . . 3 𝑥𝐴
2 dfss2f.2 . . 3 𝑥𝐵
31, 2dfss2f 3884 . 2 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
4 df-ral 3075 . 2 (∀𝑥𝐴 𝑥𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
53, 4bitr4i 281 1 (𝐴𝐵 ↔ ∀𝑥𝐴 𝑥𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1536   ∈ wcel 2111  Ⅎwnfc 2899  ∀wral 3070   ⊆ wss 3860 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-11 2158  ax-12 2175  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ral 3075  df-v 3411  df-in 3867  df-ss 3877 This theorem is referenced by:  nfss  3886  sigaclcu2  31611  bnj1498  32565  heibor1  35554  ssrabf  42151  ssrab2f  42153  limsupequzmpt2  42754  liminfequzmpt2  42827  pimconstlt1  43734  pimltpnf  43735  pimiooltgt  43740  pimdecfgtioc  43744  pimincfltioc  43745  pimdecfgtioo  43746  pimincfltioo  43747  sssmf  43766
 Copyright terms: Public domain W3C validator