Theorem ralbii 2444

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

Syntax hints:   ↔ wb 104  ⊤wtru 1333  ∀wral 2417

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-4 1488  ax-17 1507

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-ral 2422

This theorem is referenced by:  2ralbii  2446  ralinexa  2465  r3al  2480  r19.26-2  2564  r19.26-3  2565  ralbiim  2569  r19.28av  2571  ralnex2  2574  cbvral2v  2668  cbvral3v  2670  sbralie  2673  ralcom4  2711  reu8  2884  2reuswapdc  2892  r19.12sn  3597  eqsnm  3690  uni0b  3769  uni0c  3770  ssint  3795  iuniin  3831  iuneq2  3837  iunss  3862  ssiinf  3870  iinab  3882  iindif2m  3888  iinin2m  3889  iinuniss  3903  sspwuni  3905  iinpw  3911  dftr3  4038  trint  4049  bnd2  4105  reusv3  4389  reg2exmidlema  4457  setindel  4461  ordsoexmid  4485  zfregfr  4496  tfi  4504  tfis2f  4506  ssrel2  4637  reliun  4668  xpiindim  4684  ralxpf  4693  dfse2  4920  rninxp  4990  dminxp  4991  cnviinm  5088  cnvpom  5089  cnvsom  5090  dffun9  5160  funco  5171  funcnv3  5193  fncnv  5197  funimaexglem  5214  fnres  5247  fnopabg  5254  mptfng  5256  fintm  5316  f1ompt  5579  idref  5666  dff13f  5679  foov  5925  tfr1onlemaccex  6253  tfrcllembxssdm  6261  tfrcllemaccex  6266  oacl  6364  ixpeq2  6614  ixpin  6625  ixpiinm  6626  infmoti  6923  acfun  7080  ccfunen  7096  cc2  7099  cc4f  7101  cc4n  7103  cauappcvgprlemladdrl  7489  axcaucvglemres  7731  axpre-suploc  7734  dfinfre  8738  suprzclex  9173  supinfneg  9417  infsupneg  9418  cvg1nlemcau  10788  cvg1nlemres  10789  rexfiuz  10793  recvguniq  10799  resqrexlemglsq  10826  resqrexlemsqa  10828  resqrexlemex  10829  clim0  11086  mertenslem2  11337  infssuzex  11678  bezoutlemmain  11722  ennnfoneleminc  11960  ennnfonelemex  11963  ennnfonelemhom  11964  ennnfonelemr  11972  ctinfom  11977  isbasis2g  12251  tgval2  12259  ntreq0  12340  lmres  12456  eltx  12467  suplociccreex  12810  decidi  13173  nninfsellemqall  13386  nninfomni  13390  trirec0xor  13413