Theorem reubii 3267

Description: Formula-building rule for restricted existential quantifier (inference rule). (Contributed by NM, 22-Oct-1999.)

Hypothesis

Ref	Expression
reubii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
reubii	⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐴 𝜓)

Proof of Theorem reubii

Step	Hyp	Ref	Expression
1		reubii.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	a1i 11	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓))
3	2	reubiia 3266	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐴 𝜓)

Syntax hints:   ↔ wb 196   ∈ wcel 2139  ∃!wreu 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-12 2196

This theorem depends on definitions:  df-bi 197  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-eu 2611  df-reu 3057

This theorem is referenced by:  2reu5lem1  3554  reusv2lem5  5022  reusv2  5023  oaf1o  7814  aceq2  9152  lubfval  17199  lubeldm  17202  glbfval  17212  glbeldm  17215  oduglb  17360  odulub  17362  usgredg2vlem1  26337  usgredg2vlem2  26338  frcond1  27441  frcond2  27442  n4cyclfrgr  27466  cnlnadjlem3  29258  disjrdx  29732  lshpsmreu  34917  2reu7  41715  2reu8  41716