Theorem reubii 3375

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

Syntax hints:   ↔ wb 208   ∈ wcel 2141  ∃!wreu 3364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-mo 2565  df-eu 2595  df-reu 3367

This theorem is referenced by:  2reu5lem1  3716  reusv2lem5  5356  reusv2  5357  oaf1o  8526  aceq2  10069  lubfval  18371  lubeldm  18374  glbfval  18384  glbeldm  18387  odulub  18428  oduglb  18430  2sqreu  27508  2sqreunn  27509  2sqreult  27510  2sqreultb  27511  2sqreunnlt  27512  2sqreunnltb  27513  uspgredgiedg  29333  uspgriedgedg  29334  usgredg2vlem1  29383  usgredg2vlem2  29384  frcond1  30425  frcond2  30426  n4cyclfrgr  30450  cnlnadjlem3  32229  disjrdx  32751  ply1divalg3  35953  lshpsmreu  39694  reuf1odnf  47662  reuf1od  47663  2reu7  47666  2reu8  47667  2reu8i  47668  2reuimp0  47669  isuspgrim0  48477  isuspgrimlem  48478  uptr2  49803