Theorem birex 1224

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

Hypothesis

Ref	Expression
biral.1	⊢ (φ ↔ ψ)

Assertion

Ref	Expression
birex	⊢ (∃x ∈ A φ ↔ ∃x ∈ A ψ)

WTD>2

Proof of Theorem birex

Step	Hyp	Ref	Expression
1		pm4.2 148	. 2 ⊢ (φ ↔ φ)
1	hbth 697	. . 3 ⊢ ((φ ↔ φ) → ∀x(φ ↔ φ))
3		biral.1	. . . 4 ⊢ (φ ↔ ψ)
4	3	a1i 7	. . 3 ⊢ ((φ ↔ φ) → (φ ↔ ψ))
5	2, 4	birexd 1218	. 2 ⊢ ((φ ↔ φ) → (∃x ∈ A φ ↔ ∃x ∈ A ψ))
6	1, 5	ax-mp 6	1 ⊢ (∃x ∈ A φ ↔ ∃x ∈ A ψ)

Syntax hints:   ↔ wb 127  ∃wrex 1202

This theorem is referenced by:  bi2rex 1226  r19.29r 1296  r19.42v 1303  reeanv 1316  rexcom4 1361  reuxfr 1580  0el 1720  uni0b 1939  iuniin 2001  iunrab 2022  iinss 2025  iunn0 2029  iunin2 2030  iundif2 2032  iununi 2037  iunpwss 2039  iunpw 2040  dffr2 2171  dfepfr 2184  epfrc 2185  sucel 2296  cnvuni 2521  dffr3 2620  imaiun 2650  abrexexlem2 2911  abrexex2 2915  rdglem1 2975  elrnoprab 3054  qsid 3237  prfi 3444  zfregcl 3446  zfreg 3447  zfreg2 3448  kmlem7 3586  kmlem12 3591  numth2 3600  zorn2 3612  isinfcard 3692  nnwof 4609  climunii 4883  hlimunii 5143  shne0 5372

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  df-ex 679  df-rex 1206

metamath.org