Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > reubii | Structured version Visualization version GIF version |
Description: Formula-building rule for restricted existential quantifier (inference rule). (Contributed by NM, 22-Oct-1999.) |
Ref | Expression |
---|---|
reubii.1 | ⊢ (𝜑 ↔ 𝜓) |
Ref | Expression |
---|---|
reubii | ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐴 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reubii.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
2 | 1 | a1i 11 | . 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓)) |
3 | 2 | reubiia 3104 | 1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐴 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 ∈ wcel 1977 ∃!wreu 2898 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-12 2034 |
This theorem depends on definitions: df-bi 196 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-eu 2462 df-reu 2903 |
This theorem is referenced by: 2reu5lem1 3380 reusv2lem5 4799 reusv2 4800 oaf1o 7530 aceq2 8825 lubfval 16801 lubeldm 16804 glbfval 16814 glbeldm 16817 oduglb 16962 odulub 16964 usgraidx2vlem1 25920 usgraidx2vlem2 25921 frgraunss 26522 frgraun 26523 n4cyclfrgra 26545 cnlnadjlem3 28312 disjrdx 28786 lshpsmreu 33414 2reu7 39840 2reu8 39841 usgredg2vlem1 40452 usgredg2vlem2 40453 frcond1 41438 frcond2 41439 n4cyclfrgr 41461 |
Copyright terms: Public domain | W3C validator |