Theorem rabbii 3415

Description: Equivalent wff's correspond to equal restricted class abstractions. Inference form of rabbidv 3421. (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 3414	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   ↔ wb 205   = 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:  dfdif3  4055  elneldisj  4328  elnelun  4329  dfepfr  5585  epfrc  5586  fndmdifcom  6952  fniniseg2  6971  uniordint  7683  dfoi  9314  kmlem3  9954  alephsuc3  10382  hashbclem  14209  gcdcom  16265  gcdass  16300  lcmcom  16343  lcmass  16364  acsfn0  17414  dfinito2  17763  dftermo2  17764  dfrhm2  20006  lbsextg  20469  dmtopon  22117  fctop2  22200  ordtrest2  22400  qtopres  22894  tsmsfbas  23324  shftmbl  24747  ppiub  26397  rpvmasum  26719  umgrislfupgrlem  27537  finsumvtxdg2ssteplem1  27957  clwwlknclwwlkdifnum  28389  clwwlknon2num  28514  dlwwlknondlwlknonf1o  28774  numclwlk1lem1  28778  aciunf1  31045  fpwrelmapffslem  31112  ordtrest2NEW  31918  unelldsys  32171  rossros  32193  aean  32257  orvcval2  32470  subfacp1lem6  33192  satfv1  33370  noextendlt  33917  nosepne  33928  nosepdm  33932  nosupbnd2lem1  33963  noinfbnd2lem1  33978  noetasuplem4  33984  itg2addnclem2  35873  scottexf  36370  scott0f  36371  rabbieq  36433  refsymrels2  36721  dfeqvrels2  36743  refrelsredund3  36789  dffunsALTV5  36840  glbconxN  37434  3anrabdioph  40641  3orrabdioph  40642  rexrabdioph  40653  2rexfrabdioph  40655  3rexfrabdioph  40656  4rexfrabdioph  40657  6rexfrabdioph  40658  7rexfrabdioph  40659  elnn0rabdioph  40662  elnnrabdioph  40666  rabren3dioph  40674  rmydioph  40874  rmxdioph  40876  expdiophlem2  40882  relintab  41229  sqrtcvallem1  41277  uzmptshftfval  42002  binomcxplemdvsum  42011  binomcxp  42013  dvnprod  43539  ovnsubadd  44160  hoidmv1lelem3  44181  hoidmvlelem3  44185  ovolval3  44235  ovolval4lem2  44238  ovolval5lem3  44242  smflimlem4  44362