Theorem reubii 3383

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

Syntax hints:   ↔ wb 205   ∈ wcel 2104  ∃!wreu 3372

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 206  df-an 395  df-ex 1780  df-mo 2532  df-eu 2561  df-reu 3375

This theorem is referenced by:  2reu5lem1  3750  reusv2lem5  5399  reusv2  5400  oaf1o  8565  aceq2  10116  lubfval  18307  lubeldm  18310  glbfval  18320  glbeldm  18323  odulub  18364  oduglb  18366  2sqreu  27195  2sqreunn  27196  2sqreult  27197  2sqreultb  27198  2sqreunnlt  27199  2sqreunnltb  27200  usgredg2vlem1  28749  usgredg2vlem2  28750  frcond1  29786  frcond2  29787  n4cyclfrgr  29811  cnlnadjlem3  31589  disjrdx  32089  lshpsmreu  38282  reuf1odnf  46113  reuf1od  46114  2reu7  46117  2reu8  46118  2reu8i  46119  2reuimp0  46120