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

Theorem dfss3f 3974
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 3973 . 2 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
4 df-ral 3061 . 2 (∀𝑥𝐴 𝑥𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
53, 4bitr4i 278 1 (𝐴𝐵 ↔ ∀𝑥𝐴 𝑥𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wal 1537  wcel 2107  wnfc 2889  wral 3060  wss 3950
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-11 2156  ax-12 2176
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-nf 1783  df-clel 2815  df-nfc 2891  df-ral 3061  df-ss 3967
This theorem is referenced by:  nfss  3975  sigaclcu2  34122  bnj1498  35076  heibor1  37818  ssrabf  45124  ssrab2f  45127  limsupequzmpt2  45738  liminfequzmpt2  45811  pimconstlt1  46722  pimltpnff  46723  pimiooltgt  46730  pimdecfgtioc  46735  pimincfltioc  46736  pimdecfgtioo  46737  pimincfltioo  46738  pimgtmnff  46742  sssmf  46758
  Copyright terms: Public domain W3C validator