Theorem reubii 3389

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

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

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-mo 2540  df-eu 2569  df-reu 3381

This theorem is referenced by:  2reu5lem1  3761  reusv2lem5  5402  reusv2  5403  oaf1o  8601  aceq2  10159  lubfval  18395  lubeldm  18398  glbfval  18408  glbeldm  18411  odulub  18452  oduglb  18454  2sqreu  27500  2sqreunn  27501  2sqreult  27502  2sqreultb  27503  2sqreunnlt  27504  2sqreunnltb  27505  uspgredgiedg  29192  uspgriedgedg  29193  usgredg2vlem1  29242  usgredg2vlem2  29243  frcond1  30285  frcond2  30286  n4cyclfrgr  30310  cnlnadjlem3  32088  disjrdx  32604  ply1divalg3  35647  lshpsmreu  39110  reuf1odnf  47119  reuf1od  47120  2reu7  47123  2reu8  47124  2reu8i  47125  2reuimp0  47126  isuspgrim0  47872  isuspgrimlem  47874