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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2147  ∃!wreu 3367

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 1945  ax-6 2002  ax-7 2043

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-mo 2567  df-eu 2597  df-reu 3370

This theorem is used by:  2reu5lem1  3716  reusv2lem5  5371  reusv2  5372  oaf1o  8609  aceq2  10237  lubfval  18572  lubeldm  18575  glbfval  18585  glbeldm  18588  odulub  18629  oduglb  18631  2sqreu  27840  2sqreunn  27841  2sqreult  27842  2sqreultb  27843  2sqreunnlt  27844  2sqreunnltb  27845  uspgredgiedg  29813  uspgriedgedg  29814  usgredg2vlem1  29863  usgredg2vlem2  29864  frcond1  30924  frcond2  30925  n4cyclfrgr  30949  cnlnadjlem3  32728  disjrdx  33283  ply1divalg3  36615  lshpsmreu  40432  reuf1odnf  48451  reuf1od  48452  2reu7  48455  2reu8  48456  2reu8i  48457  2reuimp0  48458  isuspgrim0  49265  isuspgrimlem  49266  uptr2  50668  ralseubii  51357