Theorem reubii 3363

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

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

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 3355

This theorem is referenced by:  2reu5lem1  3726  reusv2lem5  5357  reusv2  5358  oaf1o  8527  aceq2  10072  lubfval  18309  lubeldm  18312  glbfval  18322  glbeldm  18325  odulub  18366  oduglb  18368  2sqreu  27367  2sqreunn  27368  2sqreult  27369  2sqreultb  27370  2sqreunnlt  27371  2sqreunnltb  27372  uspgredgiedg  29102  uspgriedgedg  29103  usgredg2vlem1  29152  usgredg2vlem2  29153  frcond1  30195  frcond2  30196  n4cyclfrgr  30220  cnlnadjlem3  31998  disjrdx  32520  ply1divalg3  35629  lshpsmreu  39102  reuf1odnf  47108  reuf1od  47109  2reu7  47112  2reu8  47113  2reu8i  47114  2reuimp0  47115  isuspgrim0  47894  isuspgrimlem  47895  uptr2  49210