Theorem rabbii 3439

Description: Equivalent wff's correspond to equal restricted class abstractions. Inference form of rabbidv 3441. (Contributed by Peter Mazsa, 1-Nov-2019.)

Hypothesis

Ref	Expression
rabbii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
rabbii	⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓}

Proof of Theorem rabbii

Step	Hyp	Ref	Expression
1		rabbii.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	a1i 11	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓))
3	2	rabbiia 3437	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   ↔ wb 205   = wceq 1542   ∈ wcel 2107  {crab 3433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-rab 3434

This theorem is referenced by:  dfdif3  4115  elneldisj  4389  elnelun  4390  dfepfr  5662  epfrc  5663  fndmdifcom  7045  fniniseg2  7064  uniordint  7789  naddov3  8679  dfoi  9506  kmlem3  10147  alephsuc3  10575  hashbclem  14411  gcdcom  16454  gcdass  16489  lcmcom  16530  lcmass  16551  acsfn0  17604  dfinito2  17953  dftermo2  17954  dfrhm2  20253  lbsextg  20775  dmtopon  22425  fctop2  22508  ordtrest2  22708  qtopres  23202  tsmsfbas  23632  shftmbl  25055  ppiub  26707  rpvmasum  27029  noextendlt  27172  nosepne  27183  nosepdm  27187  nosupbnd2lem1  27218  noinfbnd2lem1  27233  noetasuplem4  27239  umgrislfupgrlem  28413  finsumvtxdg2ssteplem1  28833  clwwlknclwwlkdifnum  29264  clwwlknon2num  29389  dlwwlknondlwlknonf1o  29649  numclwlk1lem1  29653  aciunf1  31919  fpwrelmapffslem  31988  ordtrest2NEW  32934  unelldsys  33187  rossros  33209  aean  33273  orvcval2  33488  subfacp1lem6  34207  satfv1  34385  itg2addnclem2  36588  scottexf  37084  scott0f  37085  rabbieq  37166  refsymrels2  37483  dfeqvrels2  37506  refrelsredund3  37552  dffunsALTV5  37605  glbconxN  38297  3anrabdioph  41568  3orrabdioph  41569  rexrabdioph  41580  2rexfrabdioph  41582  3rexfrabdioph  41583  4rexfrabdioph  41584  6rexfrabdioph  41585  7rexfrabdioph  41586  elnn0rabdioph  41589  elnnrabdioph  41593  rabren3dioph  41601  rmydioph  41801  rmxdioph  41803  expdiophlem2  41809  onuniintrab  42023  relintab  42382  sqrtcvallem1  42430  uzmptshftfval  43153  binomcxplemdvsum  43162  binomcxp  43164  dvnprod  44713  ovnsubadd  45336  hoidmv1lelem3  45357  hoidmvlelem3  45361  ovolval3  45411  ovolval4lem2  45414  ovolval5lem3  45418  smflimlem4  45538