Theorem ralbii 2514

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

Syntax hints:   ↔ wb 105  ⊤wtru 1374  ∀wral 2486

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-ral 2491

This theorem is referenced by:  2ralbii  2516  ralinexa  2535  r3al  2552  r19.26-2  2637  r19.26-3  2638  ralbiim  2642  r19.28av  2644  ralnex2  2647  ralrot3  2673  cbvral2vw  2753  cbvral2v  2755  cbvral3v  2757  sbralie  2760  ralcom4  2799  reu8  2976  2reuswapdc  2984  r19.12sn  3709  eqsnm  3809  uni0b  3889  uni0c  3890  ssint  3915  iuniin  3951  iuneq2  3957  iunss  3982  ssiinf  3991  iinab  4003  iindif2m  4009  iinin2m  4010  iinuniss  4024  sspwuni  4026  iinpw  4032  dftr3  4162  trint  4173  bnd2  4233  reusv3  4525  reg2exmidlema  4600  setindel  4604  ordsoexmid  4628  zfregfr  4640  tfi  4648  tfis2f  4650  ssrel2  4783  reliun  4814  xpiindim  4833  ralxpf  4842  dfse2  5074  rninxp  5145  dminxp  5146  cnviinm  5243  cnvpom  5244  cnvsom  5245  dffun9  5319  funco  5330  funcnv3  5355  fncnv  5359  funimaexglem  5376  fnres  5412  fnopabg  5419  mptfng  5421  fintm  5483  f1ompt  5754  idref  5848  dff13f  5862  foov  6116  tfr1onlemaccex  6457  tfrcllembxssdm  6465  tfrcllemaccex  6470  oacl  6569  ixpeq2  6822  ixpin  6833  ixpiinm  6834  infmoti  7156  acfun  7350  exmidontriimlem1  7364  exmidontriimlem3  7366  ccfunen  7411  cc2  7414  cc4f  7416  cc4n  7418  cauappcvgprlemladdrl  7805  axcaucvglemres  8047  axpre-suploc  8050  dfinfre  9064  suprzclex  9506  supinfneg  9751  infsupneg  9752  infssuzex  10413  cvg1nlemcau  11410  cvg1nlemres  11411  rexfiuz  11415  recvguniq  11421  resqrexlemglsq  11448  resqrexlemsqa  11450  resqrexlemex  11451  clim0  11711  mertenslem2  11962  bezoutlemmain  12434  ennnfoneleminc  12897  ennnfonelemex  12900  ennnfonelemhom  12901  ennnfonelemr  12909  ctinfom  12914  isnsg2  13654  isbasis2g  14632  tgval2  14638  ntreq0  14719  lmres  14835  eltx  14846  suplociccreex  15211  lgseisenlem2  15663  decidi  15931  nninfsellemqall  16154  nninfomni  16158  trirec0xor  16186