Theorem reubii 3352

Description: Formula-building rule for restricted existential uniqueness 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 3350	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐴 𝜓)

Syntax hints:   ↔ wb 206   ∈ wcel 2114  ∃!wreu 3341

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-mo 2540  df-eu 2570  df-reu 3344

This theorem is referenced by:  2reu5lem1  3702  reusv2lem5  5339  reusv2  5340  oaf1o  8491  aceq2  10032  lubfval  18305  lubeldm  18308  glbfval  18318  glbeldm  18321  odulub  18362  oduglb  18364  2sqreu  27433  2sqreunn  27434  2sqreult  27435  2sqreultb  27436  2sqreunnlt  27437  2sqreunnltb  27438  uspgredgiedg  29258  uspgriedgedg  29259  usgredg2vlem1  29308  usgredg2vlem2  29309  frcond1  30351  frcond2  30352  n4cyclfrgr  30376  cnlnadjlem3  32155  disjrdx  32676  ply1divalg3  35840  lshpsmreu  39569  reuf1odnf  47567  reuf1od  47568  2reu7  47571  2reu8  47572  2reu8i  47573  2reuimp0  47574  isuspgrim0  48382  isuspgrimlem  48383  uptr2  49708