Theorem rabbii 3405

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

Syntax hints:   ↔ wb 205   = wceq 1541   ∈ wcel 2109  {crab 3069

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-rab 3074

This theorem is referenced by:  dfdif3  4053  elneldisj  4327  elnelun  4328  dfepfr  5573  epfrc  5574  fndmdifcom  6914  fniniseg2  6933  uniordint  7641  dfoi  9231  kmlem3  9892  alephsuc3  10320  hashbclem  14145  gcdcom  16201  gcdass  16236  lcmcom  16279  lcmass  16300  acsfn0  17350  dfinito2  17699  dftermo2  17700  dfrhm2  19942  lbsextg  20405  dmtopon  22053  fctop2  22136  ordtrest2  22336  qtopres  22830  tsmsfbas  23260  shftmbl  24683  ppiub  26333  rpvmasum  26655  umgrislfupgrlem  27473  finsumvtxdg2ssteplem1  27893  clwwlknclwwlkdifnum  28323  clwwlknon2num  28448  dlwwlknondlwlknonf1o  28708  numclwlk1lem1  28712  aciunf1  30979  fpwrelmapffslem  31046  ordtrest2NEW  31852  unelldsys  32105  rossros  32127  aean  32191  orvcval2  32404  subfacp1lem6  33126  satfv1  33304  noextendlt  33851  nosepne  33862  nosepdm  33866  nosupbnd2lem1  33897  noinfbnd2lem1  33912  noetasuplem4  33918  itg2addnclem2  35808  scottexf  36305  scott0f  36306  rabbieq  36369  refsymrels2  36658  dfeqvrels2  36680  refrelsredund3  36726  dffunsALTV5  36777  glbconxN  37371  3anrabdioph  40584  3orrabdioph  40585  rexrabdioph  40596  2rexfrabdioph  40598  3rexfrabdioph  40599  4rexfrabdioph  40600  6rexfrabdioph  40601  7rexfrabdioph  40602  elnn0rabdioph  40605  elnnrabdioph  40609  rabren3dioph  40617  rmydioph  40816  rmxdioph  40818  expdiophlem2  40824  relintab  41144  sqrtcvallem1  41192  uzmptshftfval  41917  binomcxplemdvsum  41926  binomcxp  41928  dvnprod  43444  ovnsubadd  44064  hoidmv1lelem3  44085  hoidmvlelem3  44089  ovolval3  44139  ovolval4lem2  44142  ovolval5lem3  44146  smflimlem4  44260