Theorem reubii 3323

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

Syntax hints:   ↔ wb 205   ∈ wcel 2109  ∃!wreu 3067

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1786  df-mo 2541  df-eu 2570  df-reu 3072

This theorem is referenced by:  2reu5lem1  3693  reusv2lem5  5328  reusv2  5329  oaf1o  8370  aceq2  9859  lubfval  18049  lubeldm  18052  glbfval  18062  glbeldm  18065  odulub  18106  oduglb  18108  2sqreu  26585  2sqreunn  26586  2sqreult  26587  2sqreultb  26588  2sqreunnlt  26589  2sqreunnltb  26590  usgredg2vlem1  27573  usgredg2vlem2  27574  frcond1  28609  frcond2  28610  n4cyclfrgr  28634  cnlnadjlem3  30410  disjrdx  30909  lshpsmreu  37102  reuf1odnf  44550  reuf1od  44551  2reu7  44554  2reu8  44555  2reu8i  44556  2reuimp0  44557