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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1560   ∈ wcel 2142  {crab 3414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-rab 3415

This theorem is referenced by:  rabbidv  3421  rabeqbidva  3430  rabeqbidvaOLD  3431  rabbi2dva  4177  rabxfrd  5374  seinxp  5731  ordintdif  6397  f1oresrab  7109  onsucmin  7801  suppval1  8146  mptsuppd  8167  naddasslem1  8665  naddasslem2  8666  naddsuc2  8672  cantnflem1  9644  harsucnn  9956  dfinfre  12173  ixxin  13366  mptnn0fsuppr  14012  scshwfzeqfzo  14839  incexc2  15868  smueqlem  16524  gcdass  16581  lcmass  16648  pcneg  16910  ramval  17044  acsfn  17691  monpropd  17770  f1omvdcnv  19484  pmtrmvd  19496  submod  19609  odngen  19617  sylow3lem6  19672  efgsfo  19779  rrgsupp  20751  acsfn1p  20848  rngqiprngimf1  21370  dsmmbas2  21789  dsmmacl  21793  frlmbas  21807  frlmsslss2  21827  mplsubglem2  22052  ltbwe  22097  coe1mul2lem2  22331  scmatmats  22571  mretopd  23152  ordtbaslem  23248  ordtrest  23262  ordtrest2lem  23263  leordtval  23273  xkopt  23715  xkoco1cn  23717  xkoco2cn  23718  xkoinjcn  23747  r0cld  23798  utopsnneiplem  24307  stdbdbl  24577  minveclem3b  25490  minveclem4  25494  lhop1lem  26075  idomrootle  26233  mumul  27245  sqff1o  27246  lgsquadlem1  27444  lgsquadlem2  27445  2lgslem1a  27455  lrrecse  28035  lrrecpred  28037  plngcplem  28992  elntg2  29186  edglnl  29344  nbupgr  29545  vtxdun  29682  wwlksnextprop  30112  wpthswwlks2on  30164  rusgrnumwwlkslem  30172  rusgrnumwwlks  30177  clwlknf1oclwwlkn  30286  frcond3  30471  extwwlkfab  30554  grpoidinv2  30718  grpoinv  30728  xppreima  32847  qusker  33535  nsgqusf1olem3  33601  fedgmullem2  33927  ply1annidllem  33998  zarclsun  34167  cnvordtrestixx  34210  ordtrestNEW  34218  ordtrest2NEWlem  34219  fnrelpredd  35387  fineqvnttrclse  35420  satfv1lem  35712  satefvfmla0  35768  satefvfmla1  35775  lineunray  36497  lineelsb2  36498  linecom  36500  ee7.2aOLD  36821  poimirlem26  38145  poimirlem27  38146  mbfposadd  38166  cnambfre  38167  itg2addnclem2  38171  iblabsnclem  38182  ftc1anclem1  38192  lfl1dim2N  39746  pmapat  40387  pmapglbx  40393  dvhb1dimN  41610  dia0  41676  mapdval2N  42254  mapdsn  42265  hlhilocv  42581  isprimroot  42710  aks6d1c6isolem3  42793  unitscyglem5  42816  istopclsd  43281  diophren  43390  rabrenfdioph  43391  pwfi2f1o  43673  idomodle  43768  hausgraph  43782  nadd1rabtr  43965  nadd1rabex  43967  nadd1suc  43969  minregex2  44111  fsovcnvlem  44589  ntrneifv3  44658  ntrneifv4  44661  clsneifv3  44686  clsneifv4  44687  neicvgfv  44697  nzss  44893  preimaiocmnf  46136  preimaicomnf  47285  smfsupxr  47390  smfliminflem  47404  sprvalpwle2  48095  fpprmod  48349  dfsclnbgr2  48468  dfvopnbgr2  48475  uspgrlimlem2  48611  rmsupp0  48990  lco0  49049  rrxlinesc  49357  rrxlinec  49358  rrx2line  49362  rrx2vlinest  49363  rrx2linest  49364  rrx2linesl  49365  rrx2linest2  49366  2sphere  49371  2sphere0  49372  line2  49374  itsclinecirc0b  49396