Theorem ralbii 2441

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

Syntax hints:   ↔ wb 104  ⊤wtru 1332  ∀wral 2416

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 1423  ax-gen 1425  ax-4 1487  ax-17 1506

This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-ral 2421

This theorem is referenced by:  2ralbii  2443  ralinexa  2462  r3al  2477  r19.26-2  2561  r19.26-3  2562  ralbiim  2566  r19.28av  2568  ralnex2  2571  cbvral2v  2665  cbvral3v  2667  sbralie  2670  ralcom4  2708  reu8  2880  2reuswapdc  2888  r19.12sn  3589  eqsnm  3682  uni0b  3761  uni0c  3762  ssint  3787  iuniin  3823  iuneq2  3829  iunss  3854  ssiinf  3862  iinab  3874  iindif2m  3880  iinin2m  3881  iinuniss  3895  sspwuni  3897  iinpw  3903  dftr3  4030  trint  4041  bnd2  4097  reusv3  4381  reg2exmidlema  4449  setindel  4453  ordsoexmid  4477  zfregfr  4488  tfi  4496  tfis2f  4498  ssrel2  4629  reliun  4660  xpiindim  4676  ralxpf  4685  dfse2  4912  rninxp  4982  dminxp  4983  cnviinm  5080  cnvpom  5081  cnvsom  5082  dffun9  5152  funco  5163  funcnv3  5185  fncnv  5189  funimaexglem  5206  fnres  5239  fnopabg  5246  mptfng  5248  fintm  5308  f1ompt  5571  idref  5658  dff13f  5671  foov  5917  tfr1onlemaccex  6245  tfrcllembxssdm  6253  tfrcllemaccex  6258  oacl  6356  ixpeq2  6606  ixpin  6617  ixpiinm  6618  infmoti  6915  acfun  7063  ccfunen  7079  cauappcvgprlemladdrl  7465  axcaucvglemres  7707  axpre-suploc  7710  dfinfre  8714  suprzclex  9149  supinfneg  9390  infsupneg  9391  cvg1nlemcau  10756  cvg1nlemres  10757  rexfiuz  10761  recvguniq  10767  resqrexlemglsq  10794  resqrexlemsqa  10796  resqrexlemex  10797  clim0  11054  mertenslem2  11305  infssuzex  11642  bezoutlemmain  11686  ennnfoneleminc  11924  ennnfonelemex  11927  ennnfonelemhom  11928  ennnfonelemr  11936  ctinfom  11941  isbasis2g  12212  tgval2  12220  ntreq0  12301  lmres  12417  eltx  12428  suplociccreex  12771  decidi  13002  nninfsellemqall  13211  nninfomni  13215