Theorem reubii 3385

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

Syntax hints:   ↔ wb 205   ∈ wcel 2106  ∃!wreu 3374

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-mo 2534  df-eu 2563  df-reu 3377

This theorem is referenced by:  2reu5lem1  3751  reusv2lem5  5400  reusv2  5401  oaf1o  8562  aceq2  10113  lubfval  18302  lubeldm  18305  glbfval  18315  glbeldm  18318  odulub  18359  oduglb  18361  2sqreu  26956  2sqreunn  26957  2sqreult  26958  2sqreultb  26959  2sqreunnlt  26960  2sqreunnltb  26961  usgredg2vlem1  28479  usgredg2vlem2  28480  frcond1  29516  frcond2  29517  n4cyclfrgr  29541  cnlnadjlem3  31317  disjrdx  31817  lshpsmreu  37974  reuf1odnf  45805  reuf1od  45806  2reu7  45809  2reu8  45810  2reu8i  45811  2reuimp0  45812