Theorem ralbii 2538

Description: Inference adding restricted universal quantifier to both sides of an equivalence. (Contributed by NM, 23-Nov-1994.) (Revised by Mario Carneiro, 17-Oct-2016.)

Hypothesis

Ref	Expression
ralbii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
ralbii	⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)

Proof of Theorem ralbii

Step	Hyp	Ref	Expression
1		ralbii.1	. . . 4 ⊢ (𝜑 ↔ 𝜓)
2	1	a1i 9	. . 3 ⊢ (⊤ → (𝜑 ↔ 𝜓))
3	2	ralbidv 2532	. 2 ⊢ (⊤ → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓))
4	3	mptru 1406	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   ↔ wb 105  ⊤wtru 1398  ∀wral 2510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-gen 1497  ax-4 1558  ax-17 1574

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-ral 2515

This theorem is referenced by:  2ralbii  2540  ralinexa  2559  r3al  2576  r19.26-2  2662  r19.26-3  2663  ralbiim  2667  r19.28av  2669  ralnex2  2672  ralrot3  2698  cbvral2vw  2778  cbvral2v  2780  cbvral3v  2782  sbralie  2785  ralcom4  2825  reu8  3002  2reuswapdc  3010  r19.12sn  3735  eqsnm  3838  uni0b  3918  uni0c  3919  ssint  3944  iuniin  3980  iuneq2  3986  iunss  4011  ssiinf  4020  iinab  4032  iindif2m  4038  iinin2m  4039  iinuniss  4053  sspwuni  4055  iinpw  4061  dftr3  4191  trint  4202  bnd2  4263  reusv3  4557  reg2exmidlema  4632  setindel  4636  ordsoexmid  4660  zfregfr  4672  tfi  4680  tfis2f  4682  ssrel2  4816  reliun  4848  xpiindim  4867  ralxpf  4876  dfse2  5109  rninxp  5180  dminxp  5181  cnviinm  5278  cnvpom  5279  cnvsom  5280  dffun9  5355  funco  5366  funcnv3  5392  fncnv  5396  funimaexglem  5413  fnres  5449  fnopabg  5456  mptfng  5458  fintm  5522  f1ompt  5798  idref  5896  dff13f  5910  foov  6168  tfr1onlemaccex  6513  tfrcllembxssdm  6521  tfrcllemaccex  6526  oacl  6627  ixpeq2  6880  ixpin  6891  ixpiinm  6892  infmoti  7226  acfun  7421  exmidontriimlem1  7435  exmidontriimlem3  7437  ccfunen  7482  cc2  7485  cc4f  7487  cc4n  7489  cauappcvgprlemladdrl  7876  axcaucvglemres  8118  axpre-suploc  8121  dfinfre  9135  suprzclex  9577  supinfneg  9828  infsupneg  9829  infssuzex  10492  cvg1nlemcau  11544  cvg1nlemres  11545  rexfiuz  11549  recvguniq  11555  resqrexlemglsq  11582  resqrexlemsqa  11584  resqrexlemex  11585  clim0  11845  mertenslem2  12096  bezoutlemmain  12568  ennnfoneleminc  13031  ennnfonelemex  13034  ennnfonelemhom  13035  ennnfonelemr  13043  ctinfom  13048  isnsg2  13789  isbasis2g  14768  tgval2  14774  ntreq0  14855  lmres  14971  eltx  14982  suplociccreex  15347  lgseisenlem2  15799  vtxd0nedgbfi  16149  decidi  16391  nninfsellemqall  16617  nninfomni  16621  trirec0xor  16649