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  5897  dff13f  5911  foov  6169  tfr1onlemaccex  6514  tfrcllembxssdm  6522  tfrcllemaccex  6527  oacl  6628  ixpeq2  6881  ixpin  6892  ixpiinm  6893  infmoti  7227  acfun  7422  exmidontriimlem1  7436  exmidontriimlem3  7438  ccfunen  7483  cc2  7486  cc4f  7488  cc4n  7490  cauappcvgprlemladdrl  7877  axcaucvglemres  8119  axpre-suploc  8122  dfinfre  9136  suprzclex  9578  supinfneg  9829  infsupneg  9830  infssuzex  10494  cvg1nlemcau  11562  cvg1nlemres  11563  rexfiuz  11567  recvguniq  11573  resqrexlemglsq  11600  resqrexlemsqa  11602  resqrexlemex  11603  clim0  11863  mertenslem2  12115  bezoutlemmain  12587  ennnfoneleminc  13050  ennnfonelemex  13053  ennnfonelemhom  13054  ennnfonelemr  13062  ctinfom  13067  isnsg2  13808  isbasis2g  14788  tgval2  14794  ntreq0  14875  lmres  14991  eltx  15002  suplociccreex  15367  lgseisenlem2  15819  vtxd0nedgbfi  16169  decidi  16442  nninfsellemqall  16668  nninfomni  16672  trirec0xor  16700