Theorem reubii 3360

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

Hypothesis

Ref	Expression
rmobii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

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

Proof of Theorem reubii

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

Syntax hints:   ↔ wb 206   ∈ wcel 2109  ∃!wreu 3349

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-mo 2533  df-eu 2562  df-reu 3352

This theorem is referenced by:  2reu5lem1  3723  reusv2lem5  5352  reusv2  5353  oaf1o  8504  aceq2  10048  lubfval  18285  lubeldm  18288  glbfval  18298  glbeldm  18301  odulub  18342  oduglb  18344  2sqreu  27343  2sqreunn  27344  2sqreult  27345  2sqreultb  27346  2sqreunnlt  27347  2sqreunnltb  27348  uspgredgiedg  29078  uspgriedgedg  29079  usgredg2vlem1  29128  usgredg2vlem2  29129  frcond1  30168  frcond2  30169  n4cyclfrgr  30193  cnlnadjlem3  31971  disjrdx  32493  ply1divalg3  35602  lshpsmreu  39075  reuf1odnf  47081  reuf1od  47082  2reu7  47085  2reu8  47086  2reu8i  47087  2reuimp0  47088  isuspgrim0  47867  isuspgrimlem  47868  uptr2  49183