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

Theorem rabbidva 3183
Description: Equivalent wff's yield equal restricted class abstractions (deduction rule). (Contributed by NM, 28-Nov-2003.)
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 ((𝜑𝑥𝐴) → (𝜓𝜒))
21ralrimiva 2963 . 2 (𝜑 → ∀𝑥𝐴 (𝜓𝜒))
3 rabbi 3115 . 2 (∀𝑥𝐴 (𝜓𝜒) ↔ {𝑥𝐴𝜓} = {𝑥𝐴𝜒})
42, 3sylib 208 1 (𝜑 → {𝑥𝐴𝜓} = {𝑥𝐴𝜒})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1481  wcel 1988  wral 2909  {crab 2913
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-ral 2914  df-rab 2918
This theorem is referenced by:  rabbidv  3184  rabeqbidva  3191  rabbi2dva  3813  rabxfrd  4880  seinxp  5175  ordintdif  5762  f1oresrab  6381  onsucmin  7006  suppval1  7286  mptsuppd  7303  cantnflem1  8571  dfinfre  10989  ixxin  12177  mptnn0fsuppr  12782  scshwfzeqfzo  13553  incexc2  14551  smueqlem  15193  gcdass  15245  lcmass  15308  pcneg  15559  ramval  15693  acsfn  16301  monpropd  16378  f1omvdcnv  17845  pmtrmvd  17857  submod  17965  odngen  17973  sylow3lem6  18028  efgsfo  18133  rrgsupp  19272  mplsubglem2  19417  ltbwe  19453  coe1mul2lem2  19619  dsmmbas2  20062  dsmmacl  20066  frlmbas  20080  frlmsslss2  20095  scmatmats  20298  mretopd  20877  ordtbaslem  20973  ordtrest  20987  ordtrest2lem  20988  leordtval  20998  xkopt  21439  xkoco1cn  21441  xkoco2cn  21442  xkoinjcn  21471  r0cld  21522  utopsnneiplem  22032  stdbdbl  22303  minveclem3b  23180  minveclem4  23184  lhop1lem  23757  mumul  24888  sqff1o  24889  lgsquadlem1  25086  lgsquadlem2  25087  2lgslem1a  25097  edglnl  26019  nbupgr  26221  isuvtxa  26276  vtxdun  26358  wwlksnextprop  26788  wpthswwlks2on  26835  rusgrnumwwlkslem  26845  rusgrnumwwlks  26850  frcond3  27113  extwwlkfab  27194  grpoidinv2  27339  grpoinv  27349  xppreima  29422  cnvordtrestixx  29933  ordtrestNEW  29941  ordtrest2NEWlem  29942  lineunray  32229  lineelsb2  32230  linecom  32232  ee7.2aOLD  32435  poimirlem26  33406  poimirlem27  33407  mbfposadd  33428  cnambfre  33429  itg2addnclem2  33433  iblabsnclem  33444  ftc1anclem1  33456  lfl1dim2N  34228  pmapat  34868  pmapglbx  34874  dvhb1dimN  36093  dia0  36160  mapdval2N  36738  mapdsn  36749  hlhilocv  37068  istopclsd  37082  diophren  37196  rabrenfdioph  37197  pwfi2f1o  37485  acsfn1p  37588  idomrootle  37592  idomodle  37593  hausgraph  37609  fsovcnvlem  38127  ntrneifv3  38200  ntrneifv4  38203  clsneifv3  38228  clsneifv4  38229  neicvgfv  38239  nzss  38336  preimaiocmnf  39591  preimaicomnf  40685  smfsupxr  40785  smfliminflem  40799  sprvalpwle2  41504  rmsupp0  41914  lco0  41981
  Copyright terms: Public domain W3C validator