Theorem rabbidva 3420

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 580	. 2 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝜓) ↔ (𝑥 ∈ 𝐴 ∧ 𝜒)))
3	2	rabbidva2 3418	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1539   ∈ wcel 2104  {crab 3284

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 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-rab 3287

This theorem is referenced by:  rabbidv  3421  rabeqbidva  3428  rabbi2dva  4157  rabxfrd  5349  seinxp  5681  ordintdif  6330  f1oresrab  7031  onsucmin  7700  suppval1  8014  mptsuppd  8034  cantnflem1  9491  harsucnn  9800  dfinfre  12002  ixxin  13142  mptnn0fsuppr  13765  scshwfzeqfzo  14584  incexc2  15595  smueqlem  16242  gcdass  16300  lcmass  16364  pcneg  16620  ramval  16754  acsfn  17413  monpropd  17494  f1omvdcnv  19097  pmtrmvd  19109  submod  19219  odngen  19227  sylow3lem6  19282  efgsfo  19390  acsfn1p  20112  rrgsupp  20607  dsmmbas2  20989  dsmmacl  20993  frlmbas  21007  frlmsslss2  21027  mplsubglem2  21252  ltbwe  21290  coe1mul2lem2  21484  scmatmats  21705  mretopd  22288  ordtbaslem  22384  ordtrest  22398  ordtrest2lem  22399  leordtval  22409  xkopt  22851  xkoco1cn  22853  xkoco2cn  22854  xkoinjcn  22883  r0cld  22934  utopsnneiplem  23444  stdbdbl  23718  minveclem3b  24637  minveclem4  24641  lhop1lem  25222  mumul  26375  sqff1o  26376  lgsquadlem1  26573  lgsquadlem2  26574  2lgslem1a  26584  elntg2  27398  edglnl  27558  nbupgr  27756  vtxdun  27893  wwlksnextprop  28322  wpthswwlks2on  28371  rusgrnumwwlkslem  28379  rusgrnumwwlks  28384  clwlknf1oclwwlkn  28493  frcond3  28678  extwwlkfab  28761  grpoidinv2  28922  grpoinv  28932  xppreima  31028  qusker  31594  nsgqusf1olem3  31645  fedgmullem2  31756  zarclsun  31865  cnvordtrestixx  31908  ordtrestNEW  31916  ordtrest2NEWlem  31917  fnrelpredd  33106  satfv1lem  33369  satefvfmla0  33425  satefvfmla1  33432  lrrecse  34144  lrrecpred  34146  lineunray  34494  lineelsb2  34495  linecom  34497  ee7.2aOLD  34695  poimirlem26  35847  poimirlem27  35848  mbfposadd  35868  cnambfre  35869  itg2addnclem2  35873  iblabsnclem  35884  ftc1anclem1  35894  lfl1dim2N  37178  pmapat  37819  pmapglbx  37825  dvhb1dimN  39042  dia0  39108  mapdval2N  39686  mapdsn  39697  hlhilocv  40017  istopclsd  40559  diophren  40672  rabrenfdioph  40673  pwfi2f1o  40959  idomrootle  41058  idomodle  41059  hausgraph  41075  minregex2  41180  fsovcnvlem  41659  ntrneifv3  41730  ntrneifv4  41733  clsneifv3  41758  clsneifv4  41759  neicvgfv  41769  nzss  41973  preimaiocmnf  43148  preimaicomnf  44299  smfsupxr  44403  smfliminflem  44417  sprvalpwle2  44999  fpprmod  45237  rmsupp0  45762  lco0  45826  rrxlinesc  46139  rrxlinec  46140  rrx2line  46144  rrx2vlinest  46145  rrx2linest  46146  rrx2linesl  46147  rrx2linest2  46148  2sphere  46153  2sphere0  46154  line2  46156  itsclinecirc0b  46178