Theorem reubii 3386

Description: Formula-building rule for restricted existential 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 205   ∈ wcel 2107  ∃!wreu 3375

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

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-mo 2535  df-eu 2564  df-reu 3378

This theorem is referenced by:  2reu5lem1  3752  reusv2lem5  5401  reusv2  5402  oaf1o  8563  aceq2  10114  lubfval  18303  lubeldm  18306  glbfval  18316  glbeldm  18319  odulub  18360  oduglb  18362  2sqreu  26959  2sqreunn  26960  2sqreult  26961  2sqreultb  26962  2sqreunnlt  26963  2sqreunnltb  26964  usgredg2vlem1  28482  usgredg2vlem2  28483  frcond1  29519  frcond2  29520  n4cyclfrgr  29544  cnlnadjlem3  31322  disjrdx  31822  lshpsmreu  37979  reuf1odnf  45815  reuf1od  45816  2reu7  45819  2reu8  45820  2reu8i  45821  2reuimp0  45822