Theorem ralbii 2512

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 2506	. 2 ⊢ (⊤ → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓))
4	3	mptru 1382	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   ↔ wb 105  ⊤wtru 1374  ∀wral 2484

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-ral 2489

This theorem is referenced by:  2ralbii  2514  ralinexa  2533  r3al  2550  r19.26-2  2635  r19.26-3  2636  ralbiim  2640  r19.28av  2642  ralnex2  2645  ralrot3  2671  cbvral2vw  2749  cbvral2v  2751  cbvral3v  2753  sbralie  2756  ralcom4  2794  reu8  2969  2reuswapdc  2977  r19.12sn  3699  eqsnm  3796  uni0b  3875  uni0c  3876  ssint  3901  iuniin  3937  iuneq2  3943  iunss  3968  ssiinf  3977  iinab  3989  iindif2m  3995  iinin2m  3996  iinuniss  4010  sspwuni  4012  iinpw  4018  dftr3  4146  trint  4157  bnd2  4217  reusv3  4507  reg2exmidlema  4582  setindel  4586  ordsoexmid  4610  zfregfr  4622  tfi  4630  tfis2f  4632  ssrel2  4765  reliun  4796  xpiindim  4815  ralxpf  4824  dfse2  5055  rninxp  5126  dminxp  5127  cnviinm  5224  cnvpom  5225  cnvsom  5226  dffun9  5300  funco  5311  funcnv3  5336  fncnv  5340  funimaexglem  5357  fnres  5392  fnopabg  5399  mptfng  5401  fintm  5461  f1ompt  5731  idref  5825  dff13f  5839  foov  6093  tfr1onlemaccex  6434  tfrcllembxssdm  6442  tfrcllemaccex  6447  oacl  6546  ixpeq2  6799  ixpin  6810  ixpiinm  6811  infmoti  7130  acfun  7319  exmidontriimlem1  7333  exmidontriimlem3  7335  ccfunen  7376  cc2  7379  cc4f  7381  cc4n  7383  cauappcvgprlemladdrl  7770  axcaucvglemres  8012  axpre-suploc  8015  dfinfre  9029  suprzclex  9471  supinfneg  9716  infsupneg  9717  infssuzex  10376  cvg1nlemcau  11295  cvg1nlemres  11296  rexfiuz  11300  recvguniq  11306  resqrexlemglsq  11333  resqrexlemsqa  11335  resqrexlemex  11336  clim0  11596  mertenslem2  11847  bezoutlemmain  12319  ennnfoneleminc  12782  ennnfonelemex  12785  ennnfonelemhom  12786  ennnfonelemr  12794  ctinfom  12799  isnsg2  13539  isbasis2g  14517  tgval2  14523  ntreq0  14604  lmres  14720  eltx  14731  suplociccreex  15096  lgseisenlem2  15548  decidi  15731  nninfsellemqall  15952  nninfomni  15956  trirec0xor  15984