Theorem ralbii 2503

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

Syntax hints:   ↔ wb 105  ⊤wtru 1365  ∀wral 2475

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-ral 2480

This theorem is referenced by:  2ralbii  2505  ralinexa  2524  r3al  2541  r19.26-2  2626  r19.26-3  2627  ralbiim  2631  r19.28av  2633  ralnex2  2636  ralrot3  2662  cbvral2vw  2740  cbvral2v  2742  cbvral3v  2744  sbralie  2747  ralcom4  2785  reu8  2960  2reuswapdc  2968  r19.12sn  3689  eqsnm  3786  uni0b  3865  uni0c  3866  ssint  3891  iuniin  3927  iuneq2  3933  iunss  3958  ssiinf  3967  iinab  3979  iindif2m  3985  iinin2m  3986  iinuniss  4000  sspwuni  4002  iinpw  4008  dftr3  4136  trint  4147  bnd2  4207  reusv3  4496  reg2exmidlema  4571  setindel  4575  ordsoexmid  4599  zfregfr  4611  tfi  4619  tfis2f  4621  ssrel2  4754  reliun  4785  xpiindim  4804  ralxpf  4813  dfse2  5043  rninxp  5114  dminxp  5115  cnviinm  5212  cnvpom  5213  cnvsom  5214  dffun9  5288  funco  5299  funcnv3  5321  fncnv  5325  funimaexglem  5342  fnres  5377  fnopabg  5384  mptfng  5386  fintm  5446  f1ompt  5716  idref  5806  dff13f  5820  foov  6074  tfr1onlemaccex  6415  tfrcllembxssdm  6423  tfrcllemaccex  6428  oacl  6527  ixpeq2  6780  ixpin  6791  ixpiinm  6792  infmoti  7103  acfun  7292  exmidontriimlem1  7306  exmidontriimlem3  7308  ccfunen  7349  cc2  7352  cc4f  7354  cc4n  7356  cauappcvgprlemladdrl  7743  axcaucvglemres  7985  axpre-suploc  7988  dfinfre  9002  suprzclex  9443  supinfneg  9688  infsupneg  9689  infssuzex  10342  cvg1nlemcau  11168  cvg1nlemres  11169  rexfiuz  11173  recvguniq  11179  resqrexlemglsq  11206  resqrexlemsqa  11208  resqrexlemex  11209  clim0  11469  mertenslem2  11720  bezoutlemmain  12192  ennnfoneleminc  12655  ennnfonelemex  12658  ennnfonelemhom  12659  ennnfonelemr  12667  ctinfom  12672  isnsg2  13411  isbasis2g  14389  tgval2  14395  ntreq0  14476  lmres  14592  eltx  14603  suplociccreex  14968  lgseisenlem2  15420  decidi  15549  nninfsellemqall  15770  nninfomni  15774  trirec0xor  15802