Theorem reubii 3391

Description: Formula-building rule for restricted existential quantifier (inference form). (Contributed by NM, 22-Oct-1999.)

Hypothesis

Ref	Expression
reubii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
reubii	⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐴 𝜓)

Proof of Theorem reubii

Step	Hyp	Ref	Expression
1		reubii.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	a1i 11	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓))
3	2	reubiia 3390	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐴 𝜓)

Syntax hints:   ↔ wb 208   ∈ wcel 2114  ∃!wreu 3140

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

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-mo 2622  df-eu 2654  df-reu 3145

This theorem is referenced by:  2reu5lem1  3746  reusv2lem5  5303  reusv2  5304  oaf1o  8189  aceq2  9545  lubfval  17588  lubeldm  17591  glbfval  17601  glbeldm  17604  oduglb  17749  odulub  17751  2sqreu  26032  2sqreunn  26033  2sqreult  26034  2sqreultb  26035  2sqreunnlt  26036  2sqreunnltb  26037  usgredg2vlem1  27007  usgredg2vlem2  27008  frcond1  28045  frcond2  28046  n4cyclfrgr  28070  cnlnadjlem3  29846  disjrdx  30341  lshpsmreu  36260  reuf1odnf  43326  reuf1od  43327  2reu7  43330  2reu8  43331  2reu8i  43332  2reuimp0  43333