Theorem rabbidva 3409

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 3404	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {crab 3402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-rab 3403

This theorem is referenced by:  rabbidv  3410  rabeqbidva  3419  rabeqbidvaOLD  3420  rabbi2dva  4185  rabxfrd  5367  seinxp  5715  ordintdif  6371  f1oresrab  7081  onsucmin  7776  suppval1  8122  mptsuppd  8143  naddasslem1  8635  naddasslem2  8636  naddsuc2  8642  cantnflem1  9618  harsucnn  9927  dfinfre  12140  ixxin  13299  mptnn0fsuppr  13940  scshwfzeqfzo  14768  incexc2  15780  smueqlem  16436  gcdass  16493  lcmass  16560  pcneg  16821  ramval  16955  acsfn  17596  monpropd  17675  f1omvdcnv  19350  pmtrmvd  19362  submod  19475  odngen  19483  sylow3lem6  19538  efgsfo  19645  rrgsupp  20586  acsfn1p  20684  rngqiprngimf1  21186  dsmmbas2  21622  dsmmacl  21626  frlmbas  21640  frlmsslss2  21660  mplsubglem2  21886  ltbwe  21927  coe1mul2lem2  22130  scmatmats  22374  mretopd  22955  ordtbaslem  23051  ordtrest  23065  ordtrest2lem  23066  leordtval  23076  xkopt  23518  xkoco1cn  23520  xkoco2cn  23521  xkoinjcn  23550  r0cld  23601  utopsnneiplem  24111  stdbdbl  24381  minveclem3b  25304  minveclem4  25308  lhop1lem  25894  idomrootle  26054  mumul  27067  sqff1o  27068  lgsquadlem1  27267  lgsquadlem2  27268  2lgslem1a  27278  lrrecse  27825  lrrecpred  27827  elntg2  28888  edglnl  29046  nbupgr  29247  vtxdun  29385  wwlksnextprop  29815  wpthswwlks2on  29864  rusgrnumwwlkslem  29872  rusgrnumwwlks  29877  clwlknf1oclwwlkn  29986  frcond3  30171  extwwlkfab  30254  grpoidinv2  30417  grpoinv  30427  xppreima  32542  qusker  33293  nsgqusf1olem3  33359  fedgmullem2  33599  ply1annidllem  33664  zarclsun  33833  cnvordtrestixx  33876  ordtrestNEW  33884  ordtrest2NEWlem  33885  fnrelpredd  35052  satfv1lem  35322  satefvfmla0  35378  satefvfmla1  35385  lineunray  36108  lineelsb2  36109  linecom  36111  ee7.2aOLD  36422  poimirlem26  37613  poimirlem27  37614  mbfposadd  37634  cnambfre  37635  itg2addnclem2  37639  iblabsnclem  37650  ftc1anclem1  37660  lfl1dim2N  39088  pmapat  39730  pmapglbx  39736  dvhb1dimN  40953  dia0  41019  mapdval2N  41597  mapdsn  41608  hlhilocv  41924  isprimroot  42054  aks6d1c6isolem3  42137  unitscyglem5  42160  istopclsd  42661  diophren  42774  rabrenfdioph  42775  pwfi2f1o  43058  idomodle  43153  hausgraph  43167  nadd1rabtr  43350  nadd1rabex  43352  nadd1suc  43354  minregex2  43497  fsovcnvlem  43975  ntrneifv3  44044  ntrneifv4  44047  clsneifv3  44072  clsneifv4  44073  neicvgfv  44083  nzss  44279  preimaiocmnf  45531  preimaicomnf  46682  smfsupxr  46787  smfliminflem  46801  sprvalpwle2  47463  fpprmod  47701  dfsclnbgr2  47819  dfvopnbgr2  47826  uspgrlimlem2  47961  rmsupp0  48329  lco0  48389  rrxlinesc  48697  rrxlinec  48698  rrx2line  48702  rrx2vlinest  48703  rrx2linest  48704  rrx2linesl  48705  rrx2linest2  48706  2sphere  48711  2sphere0  48712  line2  48714  itsclinecirc0b  48736