Theorem reubii 3368

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

Syntax hints:   ↔ wb 206   ∈ wcel 2108  ∃!wreu 3357

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 2539  df-eu 2568  df-reu 3360

This theorem is referenced by:  2reu5lem1  3738  reusv2lem5  5372  reusv2  5373  oaf1o  8575  aceq2  10133  lubfval  18360  lubeldm  18363  glbfval  18373  glbeldm  18376  odulub  18417  oduglb  18419  2sqreu  27419  2sqreunn  27420  2sqreult  27421  2sqreultb  27422  2sqreunnlt  27423  2sqreunnltb  27424  uspgredgiedg  29154  uspgriedgedg  29155  usgredg2vlem1  29204  usgredg2vlem2  29205  frcond1  30247  frcond2  30248  n4cyclfrgr  30272  cnlnadjlem3  32050  disjrdx  32572  ply1divalg3  35664  lshpsmreu  39127  reuf1odnf  47136  reuf1od  47137  2reu7  47140  2reu8  47141  2reu8i  47142  2reuimp0  47143  isuspgrim0  47907  isuspgrimlem  47908