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

Theorem dfss3f 3940
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 3939 . 2 (𝐴𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
4 df-ral 3066 . 2 (∀𝑥𝐴 𝑥𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
53, 4bitr4i 278 1 (𝐴𝐵 ↔ ∀𝑥𝐴 𝑥𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wal 1540  wcel 2107  wnfc 2888  wral 3065  wss 3915
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-11 2155  ax-12 2172  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ral 3066  df-v 3450  df-in 3922  df-ss 3932
This theorem is referenced by:  nfss  3941  sigaclcu2  32759  bnj1498  33713  heibor1  36298  ssrabf  43398  ssrab2f  43401  limsupequzmpt2  44033  liminfequzmpt2  44106  pimconstlt1  45017  pimltpnff  45018  pimiooltgt  45025  pimdecfgtioc  45030  pimincfltioc  45031  pimdecfgtioo  45032  pimincfltioo  45033  pimgtmnff  45037  sssmf  45053
  Copyright terms: Public domain W3C validator