Theorem ralbii 2548

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

Syntax hints:   ↔ wb 105  ⊤wtru 1399  ∀wral 2520

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-ral 2525

This theorem is referenced by:  2ralbii  2550  ralinexa  2569  r3al  2586  r19.26-2  2672  r19.26-3  2673  ralbiim  2677  r19.28av  2679  ralnex2  2682  ralrot3  2708  cbvral2vw  2789  cbvral2v  2791  cbvral3v  2793  sbralie  2796  ralcom4  2836  reu8  3013  2reuswapdc  3021  r19.12sn  3755  eqsnm  3859  uni0b  3939  uni0c  3940  ssint  3965  iuniin  4001  iuneq2  4007  iunss  4032  ssiinf  4041  iinab  4053  iindif2m  4059  iinin2m  4060  iinuniss  4074  sspwuni  4076  iinpw  4082  dftr3  4212  trint  4223  bnd2  4286  reusv3  4581  reg2exmidlema  4656  setindel  4660  ordsoexmid  4684  zfregfr  4696  tfi  4704  tfis2f  4706  ssrel2  4840  reliun  4873  xpiindim  4892  ralxpf  4901  dfse2  5135  rninxp  5206  dminxp  5207  cnviinm  5304  cnvpom  5305  cnvsom  5306  dffun9  5381  funco  5392  funcnv3  5418  fncnv  5422  funimaexglem  5439  fnres  5475  fnopabg  5482  mptfng  5484  fintm  5552  f1ompt  5828  idref  5929  dff13f  5943  foov  6201  tfr1onlemaccex  6579  tfrcllembxssdm  6587  tfrcllemaccex  6592  oacl  6693  ixpeq2  6947  ixpin  6958  ixpiinm  6959  infmoti  7319  acfun  7514  exmidontriimlem1  7528  exmidontriimlem3  7530  ccfunen  7578  cc2  7581  cc4f  7583  cc4n  7585  cauappcvgprlemladdrl  7972  axcaucvglemres  8214  axpre-suploc  8217  dfinfre  9230  suprzclex  9676  supinfneg  9927  infsupneg  9928  infssuzex  10593  hashfibc  11207  cvg1nlemcau  11669  cvg1nlemres  11670  rexfiuz  11674  recvguniq  11680  resqrexlemglsq  11707  resqrexlemsqa  11709  resqrexlemex  11710  clim0  11970  mertenslem2  12222  bezoutlemmain  12694  ennnfoneleminc  13162  ennnfonelemex  13165  ennnfonelemhom  13166  ennnfonelemr  13174  ctinfom  13179  isnsg2  13920  isbasis2g  14910  tgval2  14916  ntreq0  14997  lmres  15113  eltx  15124  suplociccreex  15489  lgseisenlem2  15944  vtxd0nedgbfi  16294  decidi  16567  nninfsellemqall  16793  nninfomni  16797  trirec0xor  16829