Theorem reubii 3359

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

Syntax hints:   ↔ wb 206   ∈ wcel 2113  ∃!wreu 3348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-mo 2539  df-eu 2569  df-reu 3351

This theorem is referenced by:  2reu5lem1  3713  reusv2lem5  5347  reusv2  5348  oaf1o  8490  aceq2  10029  lubfval  18271  lubeldm  18274  glbfval  18284  glbeldm  18287  odulub  18328  oduglb  18330  2sqreu  27423  2sqreunn  27424  2sqreult  27425  2sqreultb  27426  2sqreunnlt  27427  2sqreunnltb  27428  uspgredgiedg  29248  uspgriedgedg  29249  usgredg2vlem1  29298  usgredg2vlem2  29299  frcond1  30341  frcond2  30342  n4cyclfrgr  30366  cnlnadjlem3  32144  disjrdx  32666  ply1divalg3  35836  lshpsmreu  39369  reuf1odnf  47353  reuf1od  47354  2reu7  47357  2reu8  47358  2reu8i  47359  2reuimp0  47360  isuspgrim0  48140  isuspgrimlem  48141  uptr2  49466