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 2098  ∃!wreu 3372

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

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-mo 2529  df-eu 2558  df-reu 3375

This theorem is referenced by:  2reu5lem1  3752  reusv2lem5  5406  reusv2  5407  oaf1o  8590  aceq2  10150  lubfval  18349  lubeldm  18352  glbfval  18362  glbeldm  18365  odulub  18406  oduglb  18408  2sqreu  27409  2sqreunn  27410  2sqreult  27411  2sqreultb  27412  2sqreunnlt  27413  2sqreunnltb  27414  uspgredgiedg  29008  uspgriedgedg  29009  usgredg2vlem1  29058  usgredg2vlem2  29059  frcond1  30096  frcond2  30097  n4cyclfrgr  30121  cnlnadjlem3  31899  disjrdx  32402  lshpsmreu  38613  reuf1odnf  46516  reuf1od  46517  2reu7  46520  2reu8  46521  2reu8i  46522  2reuimp0  46523  isuspgrim0  47248  isuspgrimlem  47250