Theorem reubii 3361

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

Syntax hints:   ↔ wb 206   ∈ wcel 2114  ∃!wreu 3350

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-mo 2540  df-eu 2570  df-reu 3353

This theorem is referenced by:  2reu5lem1  3715  reusv2lem5  5349  reusv2  5350  oaf1o  8500  aceq2  10041  lubfval  18283  lubeldm  18286  glbfval  18296  glbeldm  18299  odulub  18340  oduglb  18342  2sqreu  27435  2sqreunn  27436  2sqreult  27437  2sqreultb  27438  2sqreunnlt  27439  2sqreunnltb  27440  uspgredgiedg  29260  uspgriedgedg  29261  usgredg2vlem1  29310  usgredg2vlem2  29311  frcond1  30353  frcond2  30354  n4cyclfrgr  30378  cnlnadjlem3  32157  disjrdx  32678  ply1divalg3  35858  lshpsmreu  39485  reuf1odnf  47467  reuf1od  47468  2reu7  47471  2reu8  47472  2reu8i  47473  2reuimp0  47474  isuspgrim0  48254  isuspgrimlem  48255  uptr2  49580