Theorem rabbidva 3424

Description: Equivalent wff's yield equal restricted class abstractions (deduction form). (Contributed by NM, 28-Nov-2003.)

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	ralrimiva 3149	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝜒))
3		rabbi 3342	. 2 ⊢ (∀𝑥 ∈ 𝐴 (𝜓 ↔ 𝜒) ↔ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})
4	2, 3	sylib 219	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1522   ∈ wcel 2081  ∀wral 3105  {crab 3109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-ral 3110  df-rab 3114

This theorem is referenced by:  rabbidv  3425  rabeqbidva  3431  rabbi2dva  4118  rabxfrd  5214  seinxp  5526  ordintdif  6120  f1oresrab  6757  onsucmin  7397  suppval1  7692  mptsuppd  7709  cantnflem1  9003  dfinfre  11475  ixxin  12610  mptnn0fsuppr  13222  scshwfzeqfzo  14029  incexc2  15031  smueqlem  15677  gcdass  15729  lcmass  15792  pcneg  16044  ramval  16178  acsfn  16764  monpropd  16841  f1omvdcnv  18308  pmtrmvd  18320  submod  18429  odngen  18437  sylow3lem6  18492  efgsfo  18597  acsfn1p  19273  rrgsupp  19758  mplsubglem2  19909  ltbwe  19945  mhpinvcl  20027  coe1mul2lem2  20124  dsmmbas2  20568  dsmmacl  20572  frlmbas  20586  frlmsslss2  20606  scmatmats  20809  mretopd  21389  ordtbaslem  21485  ordtrest  21499  ordtrest2lem  21500  leordtval  21510  xkopt  21952  xkoco1cn  21954  xkoco2cn  21955  xkoinjcn  21984  r0cld  22035  utopsnneiplem  22544  stdbdbl  22815  minveclem3b  23719  minveclem4  23723  lhop1lem  24298  mumul  25445  sqff1o  25446  lgsquadlem1  25643  lgsquadlem2  25644  2lgslem1a  25654  elntg2  26459  edglnl  26616  nbupgr  26814  vtxdun  26951  wwlksnextprop  27383  wpthswwlks2on  27432  rusgrnumwwlkslem  27440  rusgrnumwwlks  27445  clwlknf1oclwwlkn  27555  frcond3  27745  extwwlkfab  27828  grpoidinv2  27988  grpoinv  27998  xppreima  30089  qusker  30577  fedgmullem2  30635  cnvordtrestixx  30778  ordtrestNEW  30786  ordtrest2NEWlem  30787  satfv1lem  32223  satefvfmla0  32279  satefvfmla1  32286  lineunray  33223  lineelsb2  33224  linecom  33226  ee7.2aOLD  33424  poimirlem26  34474  poimirlem27  34475  mbfposadd  34495  cnambfre  34496  itg2addnclem2  34500  iblabsnclem  34511  ftc1anclem1  34523  lfl1dim2N  35814  pmapat  36455  pmapglbx  36461  dvhb1dimN  37678  dia0  37744  mapdval2N  38322  mapdsn  38333  hlhilocv  38649  istopclsd  38807  diophren  38920  rabrenfdioph  38921  pwfi2f1o  39206  idomrootle  39305  idomodle  39306  hausgraph  39322  harsucnn  39413  fsovcnvlem  39869  ntrneifv3  39942  ntrneifv4  39945  clsneifv3  39970  clsneifv4  39971  neicvgfv  39981  nzss  40212  preimaiocmnf  41404  preimaicomnf  42558  smfsupxr  42658  smfliminflem  42672  sprvalpwle2  43159  fpprmod  43400  rmsupp0  43922  lco0  43988  rrxlinesc  44229  rrxlinec  44230  rrx2line  44234  rrx2vlinest  44235  rrx2linest  44236  rrx2linesl  44237  rrx2linest2  44238  2sphere  44243  2sphere0  44244  line2  44246  itsclinecirc0b  44268