Theorem reubii 3356

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

Syntax hints:   ↔ wb 206   ∈ wcel 2113  ∃!wreu 3345

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-mo 2537  df-eu 2566  df-reu 3348

This theorem is referenced by:  2reu5lem1  3710  reusv2lem5  5344  reusv2  5345  oaf1o  8487  aceq2  10021  lubfval  18262  lubeldm  18265  glbfval  18275  glbeldm  18278  odulub  18319  oduglb  18321  2sqreu  27414  2sqreunn  27415  2sqreult  27416  2sqreultb  27417  2sqreunnlt  27418  2sqreunnltb  27419  uspgredgiedg  29174  uspgriedgedg  29175  usgredg2vlem1  29224  usgredg2vlem2  29225  frcond1  30267  frcond2  30268  n4cyclfrgr  30292  cnlnadjlem3  32070  disjrdx  32592  ply1divalg3  35758  lshpsmreu  39281  reuf1odnf  47269  reuf1od  47270  2reu7  47273  2reu8  47274  2reu8i  47275  2reuimp0  47276  isuspgrim0  48056  isuspgrimlem  48057  uptr2  49382