Theorem ralbii 2472

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

Syntax hints:   ↔ wb 104  ⊤wtru 1344  ∀wral 2444

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 1435  ax-gen 1437  ax-4 1498  ax-17 1514

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-ral 2449

This theorem is referenced by:  2ralbii  2474  ralinexa  2493  r3al  2510  r19.26-2  2595  r19.26-3  2596  ralbiim  2600  r19.28av  2602  ralnex2  2605  cbvral2vw  2703  cbvral2v  2705  cbvral3v  2707  sbralie  2710  ralcom4  2748  reu8  2922  2reuswapdc  2930  r19.12sn  3642  eqsnm  3735  uni0b  3814  uni0c  3815  ssint  3840  iuniin  3876  iuneq2  3882  iunss  3907  ssiinf  3915  iinab  3927  iindif2m  3933  iinin2m  3934  iinuniss  3948  sspwuni  3950  iinpw  3956  dftr3  4084  trint  4095  bnd2  4152  reusv3  4438  reg2exmidlema  4511  setindel  4515  ordsoexmid  4539  zfregfr  4551  tfi  4559  tfis2f  4561  ssrel2  4694  reliun  4725  xpiindim  4741  ralxpf  4750  dfse2  4977  rninxp  5047  dminxp  5048  cnviinm  5145  cnvpom  5146  cnvsom  5147  dffun9  5217  funco  5228  funcnv3  5250  fncnv  5254  funimaexglem  5271  fnres  5304  fnopabg  5311  mptfng  5313  fintm  5373  f1ompt  5636  idref  5725  dff13f  5738  foov  5988  tfr1onlemaccex  6316  tfrcllembxssdm  6324  tfrcllemaccex  6329  oacl  6428  ixpeq2  6678  ixpin  6689  ixpiinm  6690  infmoti  6993  acfun  7163  exmidontriimlem1  7177  exmidontriimlem3  7179  ccfunen  7205  cc2  7208  cc4f  7210  cc4n  7212  cauappcvgprlemladdrl  7598  axcaucvglemres  7840  axpre-suploc  7843  dfinfre  8851  suprzclex  9289  supinfneg  9533  infsupneg  9534  cvg1nlemcau  10926  cvg1nlemres  10927  rexfiuz  10931  recvguniq  10937  resqrexlemglsq  10964  resqrexlemsqa  10966  resqrexlemex  10967  clim0  11226  mertenslem2  11477  infssuzex  11882  bezoutlemmain  11931  ennnfoneleminc  12344  ennnfonelemex  12347  ennnfonelemhom  12348  ennnfonelemr  12356  ctinfom  12361  isbasis2g  12683  tgval2  12691  ntreq0  12772  lmres  12888  eltx  12899  suplociccreex  13242  decidi  13676  nninfsellemqall  13895  nninfomni  13899  trirec0xor  13924