Theorem ralbii 2536

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

Syntax hints:   ↔ wb 105  ⊤wtru 1396  ∀wral 2508

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-ral 2513

This theorem is referenced by:  2ralbii  2538  ralinexa  2557  r3al  2574  r19.26-2  2660  r19.26-3  2661  ralbiim  2665  r19.28av  2667  ralnex2  2670  ralrot3  2696  cbvral2vw  2776  cbvral2v  2778  cbvral3v  2780  sbralie  2783  ralcom4  2823  reu8  3000  2reuswapdc  3008  r19.12sn  3733  eqsnm  3836  uni0b  3916  uni0c  3917  ssint  3942  iuniin  3978  iuneq2  3984  iunss  4009  ssiinf  4018  iinab  4030  iindif2m  4036  iinin2m  4037  iinuniss  4051  sspwuni  4053  iinpw  4059  dftr3  4189  trint  4200  bnd2  4261  reusv3  4555  reg2exmidlema  4630  setindel  4634  ordsoexmid  4658  zfregfr  4670  tfi  4678  tfis2f  4680  ssrel2  4814  reliun  4846  xpiindim  4865  ralxpf  4874  dfse2  5107  rninxp  5178  dminxp  5179  cnviinm  5276  cnvpom  5277  cnvsom  5278  dffun9  5353  funco  5364  funcnv3  5389  fncnv  5393  funimaexglem  5410  fnres  5446  fnopabg  5453  mptfng  5455  fintm  5519  f1ompt  5794  idref  5892  dff13f  5906  foov  6164  tfr1onlemaccex  6509  tfrcllembxssdm  6517  tfrcllemaccex  6522  oacl  6623  ixpeq2  6876  ixpin  6887  ixpiinm  6888  infmoti  7218  acfun  7412  exmidontriimlem1  7426  exmidontriimlem3  7428  ccfunen  7473  cc2  7476  cc4f  7478  cc4n  7480  cauappcvgprlemladdrl  7867  axcaucvglemres  8109  axpre-suploc  8112  dfinfre  9126  suprzclex  9568  supinfneg  9819  infsupneg  9820  infssuzex  10483  cvg1nlemcau  11535  cvg1nlemres  11536  rexfiuz  11540  recvguniq  11546  resqrexlemglsq  11573  resqrexlemsqa  11575  resqrexlemex  11576  clim0  11836  mertenslem2  12087  bezoutlemmain  12559  ennnfoneleminc  13022  ennnfonelemex  13025  ennnfonelemhom  13026  ennnfonelemr  13034  ctinfom  13039  isnsg2  13780  isbasis2g  14759  tgval2  14765  ntreq0  14846  lmres  14962  eltx  14973  suplociccreex  15338  lgseisenlem2  15790  vtxd0nedgbfi  16105  decidi  16327  nninfsellemqall  16553  nninfomni  16557  trirec0xor  16585