Theorem reubii 3365

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

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

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 2534  df-eu 2563  df-reu 3357

This theorem is referenced by:  2reu5lem1  3729  reusv2lem5  5360  reusv2  5361  oaf1o  8530  aceq2  10079  lubfval  18316  lubeldm  18319  glbfval  18329  glbeldm  18332  odulub  18373  oduglb  18375  2sqreu  27374  2sqreunn  27375  2sqreult  27376  2sqreultb  27377  2sqreunnlt  27378  2sqreunnltb  27379  uspgredgiedg  29109  uspgriedgedg  29110  usgredg2vlem1  29159  usgredg2vlem2  29160  frcond1  30202  frcond2  30203  n4cyclfrgr  30227  cnlnadjlem3  32005  disjrdx  32527  ply1divalg3  35636  lshpsmreu  39109  reuf1odnf  47112  reuf1od  47113  2reu7  47116  2reu8  47117  2reu8i  47118  2reuimp0  47119  isuspgrim0  47898  isuspgrimlem  47899  uptr2  49214