Theorem reubii 3380

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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2146  ∃!wreu 3369

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-mo 2569  df-eu 2599  df-reu 3372

This theorem is used by:  2reu5lem1  3720  reusv2lem5  5375  reusv2  5376  oaf1o  8554  aceq2  10119  lubfval  18426  lubeldm  18429  glbfval  18439  glbeldm  18442  odulub  18483  oduglb  18485  2sqreu  27671  2sqreunn  27672  2sqreult  27673  2sqreultb  27674  2sqreunnlt  27675  2sqreunnltb  27676  uspgredgiedg  29583  uspgriedgedg  29584  usgredg2vlem1  29633  usgredg2vlem2  29634  frcond1  30688  frcond2  30689  n4cyclfrgr  30713  cnlnadjlem3  32492  disjrdx  33007  ply1divalg3  36171  lshpsmreu  39941  reuf1odnf  47902  reuf1od  47903  2reu7  47906  2reu8  47907  2reu8i  47908  2reuimp0  47909  isuspgrim0  48717  isuspgrimlem  48718  uptr2  50056  ralseubii  50668