Theorem rabbidva 3403

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113  {crab 3397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-rab 3398

This theorem is referenced by:  rabbidv  3404  rabeqbidva  3413  rabeqbidvaOLD  3414  rabbi2dva  4176  rabxfrd  5360  seinxp  5706  ordintdif  6366  f1oresrab  7070  onsucmin  7761  suppval1  8106  mptsuppd  8127  naddasslem1  8620  naddasslem2  8621  naddsuc2  8627  cantnflem1  9596  harsucnn  9908  dfinfre  12121  ixxin  13276  mptnn0fsuppr  13920  scshwfzeqfzo  14747  incexc2  15759  smueqlem  16415  gcdass  16472  lcmass  16539  pcneg  16800  ramval  16934  acsfn  17580  monpropd  17659  f1omvdcnv  19371  pmtrmvd  19383  submod  19496  odngen  19504  sylow3lem6  19559  efgsfo  19666  rrgsupp  20632  acsfn1p  20730  rngqiprngimf1  21253  dsmmbas2  21690  dsmmacl  21694  frlmbas  21708  frlmsslss2  21728  mplsubglem2  21954  ltbwe  21997  coe1mul2lem2  22208  scmatmats  22453  mretopd  23034  ordtbaslem  23130  ordtrest  23144  ordtrest2lem  23145  leordtval  23155  xkopt  23597  xkoco1cn  23599  xkoco2cn  23600  xkoinjcn  23629  r0cld  23680  utopsnneiplem  24189  stdbdbl  24459  minveclem3b  25382  minveclem4  25386  lhop1lem  25972  idomrootle  26132  mumul  27145  sqff1o  27146  lgsquadlem1  27345  lgsquadlem2  27346  2lgslem1a  27356  lrrecse  27912  lrrecpred  27914  elntg2  29007  edglnl  29165  nbupgr  29366  vtxdun  29504  wwlksnextprop  29934  wpthswwlks2on  29986  rusgrnumwwlkslem  29994  rusgrnumwwlks  29999  clwlknf1oclwwlkn  30108  frcond3  30293  extwwlkfab  30376  grpoidinv2  30539  grpoinv  30549  xppreima  32672  qusker  33379  nsgqusf1olem3  33445  fedgmullem2  33736  ply1annidllem  33807  zarclsun  33976  cnvordtrestixx  34019  ordtrestNEW  34027  ordtrest2NEWlem  34028  fnrelpredd  35196  fineqvnttrclse  35229  satfv1lem  35505  satefvfmla0  35561  satefvfmla1  35568  lineunray  36290  lineelsb2  36291  linecom  36293  ee7.2aOLD  36604  poimirlem26  37786  poimirlem27  37787  mbfposadd  37807  cnambfre  37808  itg2addnclem2  37812  iblabsnclem  37823  ftc1anclem1  37833  lfl1dim2N  39321  pmapat  39962  pmapglbx  39968  dvhb1dimN  41185  dia0  41251  mapdval2N  41829  mapdsn  41840  hlhilocv  42156  isprimroot  42286  aks6d1c6isolem3  42369  unitscyglem5  42392  istopclsd  42884  diophren  42997  rabrenfdioph  42998  pwfi2f1o  43280  idomodle  43375  hausgraph  43389  nadd1rabtr  43572  nadd1rabex  43574  nadd1suc  43576  minregex2  43718  fsovcnvlem  44196  ntrneifv3  44265  ntrneifv4  44268  clsneifv3  44293  clsneifv4  44294  neicvgfv  44304  nzss  44500  preimaiocmnf  45748  preimaicomnf  46897  smfsupxr  47002  smfliminflem  47016  sprvalpwle2  47677  fpprmod  47915  dfsclnbgr2  48034  dfvopnbgr2  48041  uspgrlimlem2  48177  rmsupp0  48556  lco0  48615  rrxlinesc  48923  rrxlinec  48924  rrx2line  48928  rrx2vlinest  48929  rrx2linest  48930  rrx2linesl  48931  rrx2linest2  48932  2sphere  48937  2sphere0  48938  line2  48940  itsclinecirc0b  48962