Theorem reubii 3374

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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2145  ∃!wreu 3363

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 2564  df-eu 2594  df-reu 3366

This theorem is used by:  2reu5lem1  3713  reusv2lem5  5367  reusv2  5368  oaf1o  8550  aceq2  10122  lubfval  18436  lubeldm  18439  glbfval  18449  glbeldm  18452  odulub  18493  oduglb  18495  2sqreu  27692  2sqreunn  27693  2sqreult  27694  2sqreultb  27695  2sqreunnlt  27696  2sqreunnltb  27697  uspgredgiedg  29635  uspgriedgedg  29636  usgredg2vlem1  29685  usgredg2vlem2  29686  frcond1  30746  frcond2  30747  n4cyclfrgr  30771  cnlnadjlem3  32550  disjrdx  33064  ply1divalg3  36221  lshpsmreu  39982  reuf1odnf  47995  reuf1od  47996  2reu7  47999  2reu8  48000  2reu8i  48001  2reuimp0  48002  isuspgrim0  48810  isuspgrimlem  48811  uptr2  50147  ralseubii  50762