Theorem ralbii 2556

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

Syntax hints:   ↔ wb 105  ⊤wtru 1403  ∀wral 2528

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-ral 2533

This theorem is referenced by:  2ralbii  2558  ralinexa  2577  r3al  2594  r19.26-2  2680  r19.26-3  2681  ralbiim  2685  r19.28av  2687  ralnex2  2690  ralrot3  2716  cbvral2vw  2797  cbvral2v  2799  cbvral3v  2801  sbralie  2804  ralcom4  2844  reu8  3022  2reuswapdc  3030  r19.12sn  3771  eqsnm  3875  uni0b  3955  uni0c  3956  ssint  3981  iuniin  4017  iuneq2  4023  iunss  4048  ssiinf  4057  iinab  4069  iindif2m  4075  iinin2m  4076  iinuniss  4090  sspwuni  4092  iinpw  4098  dftr3  4228  trint  4239  bnd2  4305  reusv3  4601  reg2exmidlema  4676  setindel  4680  ordsoexmid  4704  zfregfr  4716  tfi  4724  tfis2f  4726  ssrel2  4860  reliun  4893  xpiindim  4912  ralxpf  4921  dfse2  5155  rninxp  5226  dminxp  5227  cnviinm  5324  cnvpom  5325  cnvsom  5326  dffun9  5401  funco  5412  funcnv3  5438  fncnv  5442  funimaexglem  5459  fnres  5495  fnopabg  5502  mptfng  5504  fintm  5572  f1ompt  5850  idref  5952  dff13f  5966  foov  6226  tfr1onlemaccex  6609  tfrcllembxssdm  6617  tfrcllemaccex  6622  oacl  6723  ixpeq2  6984  ixpin  6995  ixpiinm  6996  infmoti  7358  acfun  7553  exmidontriimlem1  7567  exmidontriimlem3  7569  ccfunen  7620  cc2  7623  cc4f  7625  cc4n  7627  cauappcvgprlemladdrl  8014  axcaucvglemres  8256  axpre-suploc  8259  dfinfre  9276  suprzclex  9723  supinfneg  9974  infsupneg  9975  infssuzex  10644  hashfibc  11261  cvg1nlemcau  11728  cvg1nlemres  11729  rexfiuz  11733  recvguniq  11739  resqrexlemglsq  11766  resqrexlemsqa  11768  resqrexlemex  11769  clim0  12029  mertenslem2  12281  bezoutlemmain  12753  ballotfilem7  13257  ennnfoneleminc  13280  ennnfonelemex  13283  ennnfonelemhom  13284  ennnfonelemr  13292  ctinfom  13297  isnsg2  13983  isbasis2g  15069  tgval2  15075  ntreq0  15156  lmres  15272  eltx  15283  suplociccreex  15648  lgseisenlem2  16104  vtxd0nedgbfi  16454  decidi  16737  nninfsellemqall  16963  nninfomni  16967  trirec0xor  16999