Theorem reubii 3366

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

Syntax hints:   ↔ wb 208   ∈ wcel 2132  ∃!wreu 3355

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1790  df-mo 2556  df-eu 2586  df-reu 3358

This theorem is referenced by:  2reu5lem1  3708  reusv2lem5  5349  reusv2  5350  oaf1o  8516  aceq2  10061  lubfval  18352  lubeldm  18355  glbfval  18365  glbeldm  18368  odulub  18409  oduglb  18411  2sqreu  27486  2sqreunn  27487  2sqreult  27488  2sqreultb  27489  2sqreunnlt  27490  2sqreunnltb  27491  uspgredgiedg  29311  uspgriedgedg  29312  usgredg2vlem1  29361  usgredg2vlem2  29362  frcond1  30403  frcond2  30404  n4cyclfrgr  30428  cnlnadjlem3  32207  disjrdx  32729  ply1divalg3  35930  lshpsmreu  39671  reuf1odnf  47639  reuf1od  47640  2reu7  47643  2reu8  47644  2reu8i  47645  2reuimp0  47646  isuspgrim0  48454  isuspgrimlem  48455  uptr2  49780