Theorem reubii 3354

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 3352	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐴 𝜓)

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

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 3346

This theorem is referenced by:  2reu5lem1  3717  reusv2lem5  5344  reusv2  5345  oaf1o  8488  aceq2  10032  lubfval  18273  lubeldm  18276  glbfval  18286  glbeldm  18289  odulub  18330  oduglb  18332  2sqreu  27384  2sqreunn  27385  2sqreult  27386  2sqreultb  27387  2sqreunnlt  27388  2sqreunnltb  27389  uspgredgiedg  29139  uspgriedgedg  29140  usgredg2vlem1  29189  usgredg2vlem2  29190  frcond1  30229  frcond2  30230  n4cyclfrgr  30254  cnlnadjlem3  32032  disjrdx  32554  ply1divalg3  35634  lshpsmreu  39107  reuf1odnf  47111  reuf1od  47112  2reu7  47115  2reu8  47116  2reu8i  47117  2reuimp0  47118  isuspgrim0  47898  isuspgrimlem  47899  uptr2  49226