Theorem rabbidva 3395

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

Step	Hyp	Ref	Expression
1		rabbidva.1	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
2	1	pm5.32da 579	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ 𝜒)))
3	2	rabbidva2 3391	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {crab 3389

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-rab 3390

This theorem is referenced by:  rabbidv  3396  rabeqbidva  3405  rabeqbidvaOLD  3406  rabbi2dva  4166  rabxfrd  5359  seinxp  5715  ordintdif  6374  f1oresrab  7080  onsucmin  7772  suppval1  8116  mptsuppd  8137  naddasslem1  8630  naddasslem2  8631  naddsuc2  8637  cantnflem1  9610  harsucnn  9922  dfinfre  12137  ixxin  13315  mptnn0fsuppr  13961  scshwfzeqfzo  14788  incexc2  15803  smueqlem  16459  gcdass  16516  lcmass  16583  pcneg  16845  ramval  16979  acsfn  17625  monpropd  17704  f1omvdcnv  19419  pmtrmvd  19431  submod  19544  odngen  19552  sylow3lem6  19607  efgsfo  19714  rrgsupp  20678  acsfn1p  20776  rngqiprngimf1  21298  dsmmbas2  21717  dsmmacl  21721  frlmbas  21735  frlmsslss2  21755  mplsubglem2  21979  ltbwe  22022  coe1mul2lem2  22233  scmatmats  22476  mretopd  23057  ordtbaslem  23153  ordtrest  23167  ordtrest2lem  23168  leordtval  23178  xkopt  23620  xkoco1cn  23622  xkoco2cn  23623  xkoinjcn  23652  r0cld  23703  utopsnneiplem  24212  stdbdbl  24482  minveclem3b  25395  minveclem4  25399  lhop1lem  25980  idomrootle  26138  mumul  27144  sqff1o  27145  lgsquadlem1  27343  lgsquadlem2  27344  2lgslem1a  27354  lrrecse  27934  lrrecpred  27936  elntg2  29054  edglnl  29212  nbupgr  29413  vtxdun  29550  wwlksnextprop  29980  wpthswwlks2on  30032  rusgrnumwwlkslem  30040  rusgrnumwwlks  30045  clwlknf1oclwwlkn  30154  frcond3  30339  extwwlkfab  30422  grpoidinv2  30586  grpoinv  30596  xppreima  32718  qusker  33409  nsgqusf1olem3  33475  fedgmullem2  33774  ply1annidllem  33845  zarclsun  34014  cnvordtrestixx  34057  ordtrestNEW  34065  ordtrest2NEWlem  34066  fnrelpredd  35234  fineqvnttrclse  35268  satfv1lem  35544  satefvfmla0  35600  satefvfmla1  35607  lineunray  36329  lineelsb2  36330  linecom  36332  ee7.2aOLD  36643  poimirlem26  37967  poimirlem27  37968  mbfposadd  37988  cnambfre  37989  itg2addnclem2  37993  iblabsnclem  38004  ftc1anclem1  38014  lfl1dim2N  39568  pmapat  40209  pmapglbx  40215  dvhb1dimN  41432  dia0  41498  mapdval2N  42076  mapdsn  42087  hlhilocv  42403  isprimroot  42532  aks6d1c6isolem3  42615  unitscyglem5  42638  istopclsd  43132  diophren  43241  rabrenfdioph  43242  pwfi2f1o  43524  idomodle  43619  hausgraph  43633  nadd1rabtr  43816  nadd1rabex  43818  nadd1suc  43820  minregex2  43962  fsovcnvlem  44440  ntrneifv3  44509  ntrneifv4  44512  clsneifv3  44537  clsneifv4  44538  neicvgfv  44548  nzss  44744  preimaiocmnf  45990  preimaicomnf  47139  smfsupxr  47244  smfliminflem  47258  sprvalpwle2  47949  fpprmod  48203  dfsclnbgr2  48322  dfvopnbgr2  48329  uspgrlimlem2  48465  rmsupp0  48844  lco0  48903  rrxlinesc  49211  rrxlinec  49212  rrx2line  49216  rrx2vlinest  49217  rrx2linest  49218  rrx2linesl  49219  rrx2linest2  49220  2sphere  49225  2sphere0  49226  line2  49228  itsclinecirc0b  49250