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  3688  eqsnm  3785  uni0b  3864  uni0c  3865  ssint  3890  iuniin  3926  iuneq2  3932  iunss  3957  ssiinf  3966  iinab  3978  iindif2m  3984  iinin2m  3985  iinuniss  3999  sspwuni  4001  iinpw  4007  dftr3  4135  trint  4146  bnd2  4206  reusv3  4495  reg2exmidlema  4570  setindel  4574  ordsoexmid  4598  zfregfr  4610  tfi  4618  tfis2f  4620  ssrel2  4753  reliun  4784  xpiindim  4803  ralxpf  4812  dfse2  5042  rninxp  5113  dminxp  5114  cnviinm  5211  cnvpom  5212  cnvsom  5213  dffun9  5287  funco  5298  funcnv3  5320  fncnv  5324  funimaexglem  5341  fnres  5374  fnopabg  5381  mptfng  5383  fintm  5443  f1ompt  5713  idref  5803  dff13f  5817  foov  6070  tfr1onlemaccex  6406  tfrcllembxssdm  6414  tfrcllemaccex  6419  oacl  6518  ixpeq2  6771  ixpin  6782  ixpiinm  6783  infmoti  7094  acfun  7274  exmidontriimlem1  7288  exmidontriimlem3  7290  ccfunen  7331  cc2  7334  cc4f  7336  cc4n  7338  cauappcvgprlemladdrl  7724  axcaucvglemres  7966  axpre-suploc  7969  dfinfre  8983  suprzclex  9424  supinfneg  9669  infsupneg  9670  infssuzex  10323  cvg1nlemcau  11149  cvg1nlemres  11150  rexfiuz  11154  recvguniq  11160  resqrexlemglsq  11187  resqrexlemsqa  11189  resqrexlemex  11190  clim0  11450  mertenslem2  11701  bezoutlemmain  12165  ennnfoneleminc  12628  ennnfonelemex  12631  ennnfonelemhom  12632  ennnfonelemr  12640  ctinfom  12645  isnsg2  13333  isbasis2g  14281  tgval2  14287  ntreq0  14368  lmres  14484  eltx  14495  suplociccreex  14860  lgseisenlem2  15312  decidi  15441  nninfsellemqall  15659  nninfomni  15663  trirec0xor  15689