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

Theorem dfss3f 3987
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
StepHypRef Expression
1 dfssf.1 . . 3 𝑥𝐴
2 dfssf.2 . . 3 𝑥𝐵
31, 2dfssf 3986 . 2 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
4 df-ral 3060 . 2 (∀𝑥𝐴 𝑥𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
53, 4bitr4i 278 1 (𝐴𝐵 ↔ ∀𝑥𝐴 𝑥𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wal 1535  wcel 2106  wnfc 2888  wral 3059  wss 3963
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-11 2155  ax-12 2175
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-nf 1781  df-clel 2814  df-nfc 2890  df-ral 3060  df-ss 3980
This theorem is referenced by:  nfss  3988  sigaclcu2  34101  bnj1498  35054  heibor1  37797  ssrabf  45054  ssrab2f  45057  limsupequzmpt2  45674  liminfequzmpt2  45747  pimconstlt1  46658  pimltpnff  46659  pimiooltgt  46666  pimdecfgtioc  46671  pimincfltioc  46672  pimdecfgtioo  46673  pimincfltioo  46674  pimgtmnff  46678  sssmf  46694
  Copyright terms: Public domain W3C validator