Theorem reubii 3386

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

Syntax hints:   ↔ wb 206   ∈ wcel 2105  ∃!wreu 3375

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-mo 2537  df-eu 2566  df-reu 3378

This theorem is referenced by:  2reu5lem1  3763  reusv2lem5  5407  reusv2  5408  oaf1o  8599  aceq2  10156  lubfval  18407  lubeldm  18410  glbfval  18420  glbeldm  18423  odulub  18464  oduglb  18466  2sqreu  27514  2sqreunn  27515  2sqreult  27516  2sqreultb  27517  2sqreunnlt  27518  2sqreunnltb  27519  uspgredgiedg  29206  uspgriedgedg  29207  usgredg2vlem1  29256  usgredg2vlem2  29257  frcond1  30294  frcond2  30295  n4cyclfrgr  30319  cnlnadjlem3  32097  disjrdx  32610  ply1divalg3  35626  lshpsmreu  39090  reuf1odnf  47056  reuf1od  47057  2reu7  47060  2reu8  47061  2reu8i  47062  2reuimp0  47063  isuspgrim0  47809  isuspgrimlem  47811