Theorem reubii 3337

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

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

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 398  df-ex 1780  df-mo 2538  df-eu 2567  df-reu 3286

This theorem is referenced by:  2reu5lem1  3695  reusv2lem5  5334  reusv2  5335  oaf1o  8425  aceq2  9921  lubfval  18113  lubeldm  18116  glbfval  18126  glbeldm  18129  odulub  18170  oduglb  18172  2sqreu  26649  2sqreunn  26650  2sqreult  26651  2sqreultb  26652  2sqreunnlt  26653  2sqreunnltb  26654  usgredg2vlem1  27637  usgredg2vlem2  27638  frcond1  28675  frcond2  28676  n4cyclfrgr  28700  cnlnadjlem3  30476  disjrdx  30975  lshpsmreu  37165  reuf1odnf  44657  reuf1od  44658  2reu7  44661  2reu8  44662  2reu8i  44663  2reuimp0  44664