Theorem rabbidva 3405

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-rab 3400

This theorem is referenced by:  rabbidv  3406  rabeqbidva  3415  rabeqbidvaOLD  3416  rabbi2dva  4178  rabxfrd  5362  seinxp  5708  ordintdif  6368  f1oresrab  7072  onsucmin  7763  suppval1  8108  mptsuppd  8129  naddasslem1  8622  naddasslem2  8623  naddsuc2  8629  cantnflem1  9598  harsucnn  9910  dfinfre  12123  ixxin  13278  mptnn0fsuppr  13922  scshwfzeqfzo  14749  incexc2  15761  smueqlem  16417  gcdass  16474  lcmass  16541  pcneg  16802  ramval  16936  acsfn  17582  monpropd  17661  f1omvdcnv  19373  pmtrmvd  19385  submod  19498  odngen  19506  sylow3lem6  19561  efgsfo  19668  rrgsupp  20634  acsfn1p  20732  rngqiprngimf1  21255  dsmmbas2  21692  dsmmacl  21696  frlmbas  21710  frlmsslss2  21730  mplsubglem2  21956  ltbwe  21999  coe1mul2lem2  22210  scmatmats  22455  mretopd  23036  ordtbaslem  23132  ordtrest  23146  ordtrest2lem  23147  leordtval  23157  xkopt  23599  xkoco1cn  23601  xkoco2cn  23602  xkoinjcn  23631  r0cld  23682  utopsnneiplem  24191  stdbdbl  24461  minveclem3b  25384  minveclem4  25388  lhop1lem  25974  idomrootle  26134  mumul  27147  sqff1o  27148  lgsquadlem1  27347  lgsquadlem2  27348  2lgslem1a  27358  lrrecse  27938  lrrecpred  27940  elntg2  29058  edglnl  29216  nbupgr  29417  vtxdun  29555  wwlksnextprop  29985  wpthswwlks2on  30037  rusgrnumwwlkslem  30045  rusgrnumwwlks  30050  clwlknf1oclwwlkn  30159  frcond3  30344  extwwlkfab  30427  grpoidinv2  30590  grpoinv  30600  xppreima  32723  qusker  33430  nsgqusf1olem3  33496  fedgmullem2  33787  ply1annidllem  33858  zarclsun  34027  cnvordtrestixx  34070  ordtrestNEW  34078  ordtrest2NEWlem  34079  fnrelpredd  35247  fineqvnttrclse  35280  satfv1lem  35556  satefvfmla0  35612  satefvfmla1  35619  lineunray  36341  lineelsb2  36342  linecom  36344  ee7.2aOLD  36655  poimirlem26  37847  poimirlem27  37848  mbfposadd  37868  cnambfre  37869  itg2addnclem2  37873  iblabsnclem  37884  ftc1anclem1  37894  lfl1dim2N  39382  pmapat  40023  pmapglbx  40029  dvhb1dimN  41246  dia0  41312  mapdval2N  41890  mapdsn  41901  hlhilocv  42217  isprimroot  42347  aks6d1c6isolem3  42430  unitscyglem5  42453  istopclsd  42942  diophren  43055  rabrenfdioph  43056  pwfi2f1o  43338  idomodle  43433  hausgraph  43447  nadd1rabtr  43630  nadd1rabex  43632  nadd1suc  43634  minregex2  43776  fsovcnvlem  44254  ntrneifv3  44323  ntrneifv4  44326  clsneifv3  44351  clsneifv4  44352  neicvgfv  44362  nzss  44558  preimaiocmnf  45806  preimaicomnf  46955  smfsupxr  47060  smfliminflem  47074  sprvalpwle2  47735  fpprmod  47973  dfsclnbgr2  48092  dfvopnbgr2  48099  uspgrlimlem2  48235  rmsupp0  48614  lco0  48673  rrxlinesc  48981  rrxlinec  48982  rrx2line  48986  rrx2vlinest  48987  rrx2linest  48988  rrx2linesl  48989  rrx2linest2  48990  2sphere  48995  2sphere0  48996  line2  48998  itsclinecirc0b  49020