Theorem reubii 3397

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

Syntax hints:   ↔ wb 206   ∈ wcel 2108  ∃!wreu 3386

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-mo 2543  df-eu 2572  df-reu 3389

This theorem is referenced by:  2reu5lem1  3777  reusv2lem5  5420  reusv2  5421  oaf1o  8619  aceq2  10188  lubfval  18420  lubeldm  18423  glbfval  18433  glbeldm  18436  odulub  18477  oduglb  18479  2sqreu  27518  2sqreunn  27519  2sqreult  27520  2sqreultb  27521  2sqreunnlt  27522  2sqreunnltb  27523  uspgredgiedg  29210  uspgriedgedg  29211  usgredg2vlem1  29260  usgredg2vlem2  29261  frcond1  30298  frcond2  30299  n4cyclfrgr  30323  cnlnadjlem3  32101  disjrdx  32613  ply1divalg3  35610  lshpsmreu  39065  reuf1odnf  47022  reuf1od  47023  2reu7  47026  2reu8  47027  2reu8i  47028  2reuimp0  47029  isuspgrim0  47756  isuspgrimlem  47758