Theorem reubii 3378

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

Syntax hints:   ↔ wb 209   ∈ wcel 2143  ∃!wreu 3367

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-mo 2567  df-eu 2597  df-reu 3370

This theorem is referenced by:  2reu5lem1  3718  reusv2lem5  5373  reusv2  5374  oaf1o  8544  aceq2  10099  lubfval  18399  lubeldm  18402  glbfval  18412  glbeldm  18415  odulub  18456  oduglb  18458  2sqreu  27620  2sqreunn  27621  2sqreult  27622  2sqreultb  27623  2sqreunnlt  27624  2sqreunnltb  27625  uspgredgiedg  29525  uspgriedgedg  29526  usgredg2vlem1  29575  usgredg2vlem2  29576  frcond1  30617  frcond2  30618  n4cyclfrgr  30642  cnlnadjlem3  32421  disjrdx  32936  ply1divalg3  36134  lshpsmreu  39883  reuf1odnf  47844  reuf1od  47845  2reu7  47848  2reu8  47849  2reu8i  47850  2reuimp0  47851  isuspgrim0  48659  isuspgrimlem  48660  uptr2  49999  ralseubii  50611