Theorem reubii 3385

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

Syntax hints:   ↔ wb 209   ∈ wcel 2149  ∃!wreu 3374

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-mo 2573  df-eu 2603  df-reu 3377

This theorem is referenced by:  2reu5lem1  3727  reusv2lem5  5374  reusv2  5375  oaf1o  8547  aceq2  10102  lubfval  18403  lubeldm  18406  glbfval  18416  glbeldm  18419  odulub  18460  oduglb  18462  2sqreu  27585  2sqreunn  27586  2sqreult  27587  2sqreultb  27588  2sqreunnlt  27589  2sqreunnltb  27590  uspgredgiedg  29465  uspgriedgedg  29466  usgredg2vlem1  29515  usgredg2vlem2  29516  frcond1  30557  frcond2  30558  n4cyclfrgr  30582  cnlnadjlem3  32361  disjrdx  32876  ply1divalg3  36032  lshpsmreu  39772  reuf1odnf  47732  reuf1od  47733  2reu7  47736  2reu8  47737  2reu8i  47738  2reuimp0  47739  isuspgrim0  48547  isuspgrimlem  48548  uptr2  49883