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

Theorem rabbidva 3428
Description: Equivalent wff's yield equal restricted class abstractions (deduction form). (Contributed by NM, 28-Nov-2003.) (Proof shortened by SN, 3-Dec-2023.)
Hypothesis
Ref Expression
rabbidva.1 ((𝜑𝑥𝐴) → (𝜓𝜒))
Assertion
Ref Expression
rabbidva (𝜑 → {𝑥𝐴𝜓} = {𝑥𝐴𝜒})
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem rabbidva
StepHypRef Expression
1 rabbidva.1 . . 3 ((𝜑𝑥𝐴) → (𝜓𝜒))
21pm5.32da 582 . 2 (𝜑 → ((𝑥𝐴𝜓) ↔ (𝑥𝐴𝜒)))
32rabbidva2 3426 1 (𝜑 → {𝑥𝐴𝜓} = {𝑥𝐴𝜒})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1538  wcel 2112  {crab 3113
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-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-rab 3118
This theorem is referenced by:  rabbidv  3430  rabeqbidva  3437  rabbi2dva  4147  rabxfrd  5286  seinxp  5603  ordintdif  6212  f1oresrab  6870  onsucmin  7520  suppval1  7823  mptsuppd  7840  cantnflem1  9140  harsucnn  9415  dfinfre  11613  ixxin  12747  mptnn0fsuppr  13366  scshwfzeqfzo  14183  incexc2  15188  smueqlem  15832  gcdass  15888  lcmass  15951  pcneg  16203  ramval  16337  acsfn  16925  monpropd  17002  f1omvdcnv  18567  pmtrmvd  18579  submod  18689  odngen  18697  sylow3lem6  18752  efgsfo  18860  acsfn1p  19574  rrgsupp  20060  dsmmbas2  20429  dsmmacl  20433  frlmbas  20447  frlmsslss2  20467  mplsubglem2  20677  ltbwe  20715  coe1mul2lem2  20900  scmatmats  21119  mretopd  21700  ordtbaslem  21796  ordtrest  21810  ordtrest2lem  21811  leordtval  21821  xkopt  22263  xkoco1cn  22265  xkoco2cn  22266  xkoinjcn  22295  r0cld  22346  utopsnneiplem  22856  stdbdbl  23127  minveclem3b  24035  minveclem4  24039  lhop1lem  24619  mumul  25769  sqff1o  25770  lgsquadlem1  25967  lgsquadlem2  25968  2lgslem1a  25978  elntg2  26782  edglnl  26939  nbupgr  27137  vtxdun  27274  wwlksnextprop  27701  wpthswwlks2on  27750  rusgrnumwwlkslem  27758  rusgrnumwwlks  27763  clwlknf1oclwwlkn  27872  frcond3  28057  extwwlkfab  28140  grpoidinv2  28301  grpoinv  28311  xppreima  30411  qusker  30972  fedgmullem2  31114  zarclsun  31223  cnvordtrestixx  31264  ordtrestNEW  31272  ordtrest2NEWlem  31273  satfv1lem  32717  satefvfmla0  32773  satefvfmla1  32780  lineunray  33716  lineelsb2  33717  linecom  33719  ee7.2aOLD  33917  poimirlem26  35076  poimirlem27  35077  mbfposadd  35097  cnambfre  35098  itg2addnclem2  35102  iblabsnclem  35113  ftc1anclem1  35123  lfl1dim2N  36411  pmapat  37052  pmapglbx  37058  dvhb1dimN  38275  dia0  38341  mapdval2N  38919  mapdsn  38930  hlhilocv  39246  istopclsd  39628  diophren  39741  rabrenfdioph  39742  pwfi2f1o  40027  idomrootle  40126  idomodle  40127  hausgraph  40143  fsovcnvlem  40701  ntrneifv3  40772  ntrneifv4  40775  clsneifv3  40800  clsneifv4  40801  neicvgfv  40811  nzss  41008  preimaiocmnf  42185  preimaicomnf  43334  smfsupxr  43434  smfliminflem  43448  sprvalpwle2  43993  fpprmod  44232  rmsupp0  44757  lco0  44823  rrxlinesc  45136  rrxlinec  45137  rrx2line  45141  rrx2vlinest  45142  rrx2linest  45143  rrx2linesl  45144  rrx2linest2  45145  2sphere  45150  2sphere0  45151  line2  45153  itsclinecirc0b  45175
  Copyright terms: Public domain W3C validator