| 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 uniqueness quantifier (inference form). (Contributed by NM, 22-Oct-1999.) |
| Ref | Expression |
|---|---|
| rmobii.1 | ⊢ (𝜑 ↔ 𝜓) |
| Ref | Expression |
|---|---|
| reubii | ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐴 𝜓) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rmobii.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
| 2 | 1 | a1i 11 | . 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓)) |
| 3 | 2 | reubiia 3373 | 1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐴 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 208 ∈ wcel 2141 ∃!wreu 3364 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 |
| This theorem depends on definitions: df-bi 209 df-an 400 df-ex 1799 df-mo 2565 df-eu 2595 df-reu 3367 |
| This theorem is referenced by: 2reu5lem1 3716 reusv2lem5 5356 reusv2 5357 oaf1o 8526 aceq2 10069 lubfval 18371 lubeldm 18374 glbfval 18384 glbeldm 18387 odulub 18428 oduglb 18430 2sqreu 27508 2sqreunn 27509 2sqreult 27510 2sqreultb 27511 2sqreunnlt 27512 2sqreunnltb 27513 uspgredgiedg 29333 uspgriedgedg 29334 usgredg2vlem1 29383 usgredg2vlem2 29384 frcond1 30425 frcond2 30426 n4cyclfrgr 30450 cnlnadjlem3 32229 disjrdx 32751 ply1divalg3 35953 lshpsmreu 39694 reuf1odnf 47662 reuf1od 47663 2reu7 47666 2reu8 47667 2reu8i 47668 2reuimp0 47669 isuspgrim0 48477 isuspgrimlem 48478 uptr2 49803 |
| Copyright terms: Public domain | W3C validator |