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 2144  ∃!wreu 3363

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-mo 2564  df-eu 2594  df-reu 3366

This theorem is used by:  2reu5lem1  3712  reusv2lem5  5363  reusv2  5364  oaf1o  8576  aceq2  10203  lubfval  18529  lubeldm  18532  glbfval  18542  glbeldm  18545  odulub  18586  oduglb  18588  2sqreu  27790  2sqreunn  27791  2sqreult  27792  2sqreultb  27793  2sqreunnlt  27794  2sqreunnltb  27795  uspgredgiedg  29763  uspgriedgedg  29764  usgredg2vlem1  29813  usgredg2vlem2  29814  frcond1  30874  frcond2  30875  n4cyclfrgr  30899  cnlnadjlem3  32678  disjrdx  33234  ply1divalg3  36495  lshpsmreu  40273  reuf1odnf  48284  reuf1od  48285  2reu7  48288  2reu8  48289  2reu8i  48290  2reuimp0  48291  isuspgrim0  49099  isuspgrimlem  49100  uptr2  50444  ralseubii  51111