Theorem reubii 3351

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

Syntax hints:   ↔ wb 206   ∈ wcel 2114  ∃!wreu 3340

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-mo 2539  df-eu 2569  df-reu 3343

This theorem is referenced by:  2reu5lem1  3701  reusv2lem5  5344  reusv2  5345  oaf1o  8498  aceq2  10041  lubfval  18314  lubeldm  18317  glbfval  18327  glbeldm  18330  odulub  18371  oduglb  18373  2sqreu  27419  2sqreunn  27420  2sqreult  27421  2sqreultb  27422  2sqreunnlt  27423  2sqreunnltb  27424  uspgredgiedg  29244  uspgriedgedg  29245  usgredg2vlem1  29294  usgredg2vlem2  29295  frcond1  30336  frcond2  30337  n4cyclfrgr  30361  cnlnadjlem3  32140  disjrdx  32661  ply1divalg3  35824  lshpsmreu  39555  reuf1odnf  47555  reuf1od  47556  2reu7  47559  2reu8  47560  2reu8i  47561  2reuimp0  47562  isuspgrim0  48370  isuspgrimlem  48371  uptr2  49696