Theorem bial 695

Description: Inference adding universal quantifier to both sides of an equivalence.

Hypothesis

Ref	Expression
bial.1	⊢ (φ ↔ ψ)

Assertion

Ref	Expression
bial	⊢ (∀xφ ↔ ∀xψ)

Proof of Theorem bial

Step	Hyp	Ref	Expression
1		19.15 694	. 2 ⊢ (∀x(φ ↔ ψ) → (∀xφ ↔ ∀xψ))
2		bial.1	. 2 ⊢ (φ ↔ ψ)
3	1, 2	mpg 684	1 ⊢ (∀xφ ↔ ∀xψ)

Syntax hints:   ↔ wb 127  ∀wal 672

This theorem is referenced by:  bi2al 696  hbex 701  hbor 703  hban 704  hbbi 705  hb3or 706  hb3an 707  hbe1 709  alex 717  alinexa 724  exanali 725  alexn 726  19.35 754  19.30 764  19.32 765  19.31 766  19.43 767  19.41 774  albi 785  aaan 794  eqsal 833  ddelimf2 907  ddelimf 908  sbcom 916  sb8e 919  19.23vv 951  19.12vv 960  sb6a 990  sbcom2 992  sbex 998  sbalv 999  sbal2 1005  hbeu1 1015  hbeu 1016  sb8eu 1017  eu1 1019  eu2 1023  hbmo1 1032  hbmo 1033  moanim 1051  2eu3 1069  2eu4 1070  exists1 1072  axun 1081  axpow 1082  hbab1 1095  hbab 1096  cleqcom 1103  hbeq 1171  hbel 1172  cleqab 1174  cleqabr 1175  cleq2ab 1179  sbabel 1189  birala 1228  r2al 1231  hbral 1236  hbra1 1237  hbrex 1238  hbre1 1239  r3al 1240  r19.21v 1260  r19.22 1272  r19.23v 1282  r19.26 1289  hbreu1 1307  rabid2 1309  hbrab1 1310  hbrab 1311  ralcom2 1314  reu2 1338  2reuswap 1341  ralv 1357  hbsbcv 1447  rax5 1472  zfrep3 1476  zfaus 1480  nvelv 1483  dfss2 1497  hbss 1501  ss2ab 1551  ss2rab 1553  hbdif 1590  hbun 1614  ssequn1 1628  unss 1632  hbin 1647  inex1 1697  n0f 1713  disj 1733  disj2 1735  disj3 1736  ssdif0 1748  inssdif0 1754  hbpw 1804  pwex 1806  hbpr 1824  hbsn 1833  snss 1849  prsspw 1858  ssextss 1864  hbop 1879  pwpw0 1883  dtru 1889  eusn 1913  hbuni 1925  unissb 1941  uniex 1947  hbint 1975  elintrab 1977  intun 1989  intpr 1990  hbiu1 2012  hbii1 2013  dfiin2 2015  iunss 2017  ssiun 2018  ssiin 2024  iinss 2025  dftr2 2043  dftr5 2044  hbbr 2095  hbopab 2111  hbopab1 2112  hbopab2 2113  dffr2 2171  dfepfr 2184  hbsuc 2294  sucel 2296  hbxp 2444  weinxp 2467  hbrel 2478  cleqrel 2483  reluni 2493  hbco 2508  hbcnv 2516  dmopab2 2541  dm0rn0 2549  reldm0 2550  hbrn 2564  hbdm 2565  dmcosseq 2572  hbres 2577  hbima 2609  dffr3 2620  cotr 2625  intirr 2628  dffun2 2674  dffun3 2675  dffun4 2676  dffun5 2677  dffunmof 2678  hbfun 2684  dffun6 2687  funopab 2694  funcnv2 2702  funcnv 2703  fun2cnv 2704  fununi 2705  funcnvuni 2706  hbfn 2720  fnopabg 2745  hbf 2751  hbf1 2779  f11 2780  hbfo 2787  hbf1o 2798  fv2 2828  hbfv 2837  tz6.12-2 2845  elrnopab 2884  fopab2 2891  f1fv 2916  hbiso 2930  tfrlem2 2950  hbrdg 2974  abianfplem 2999  hbopr 3017  hboprab1 3023  hboprab2 3024  elrnoprab 3054  er2 3201  xpmapenlem1 3391  xpmapenlem4 3394  inf2 3459  inf4 3473  trcl 3489  setind2 3493  tz9.12lem3 3505  ranksn 3532  scottexs 3543  scott0s 3544  kardex 3550  karden 3551  aceq1 3552  aceq4 3557  aceq7 3566  ac6lem 3575  kmlem4 3583  kmlem11 3590  kmlem14 3593  kmlem15 3594  kmlem16 3595  aceqkm 3596  hta 3619  axpowndlem3 3745  zfcndrep 3760  zfcndun 3761  zfcndpow 3762  suppsr3 4018  axsup 4088  nnwos 4610  zmin 4617  om2uzsuc 4652  choc0 5291  h1deot 5454  h1det 5455

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org