| 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 3387 | 1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥 ∈ 𝐴 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ∈ wcel 2108 ∃!wreu 3378 |
| 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 207 df-an 396 df-ex 1780 df-mo 2540 df-eu 2569 df-reu 3381 |
| This theorem is referenced by: 2reu5lem1 3761 reusv2lem5 5402 reusv2 5403 oaf1o 8601 aceq2 10159 lubfval 18395 lubeldm 18398 glbfval 18408 glbeldm 18411 odulub 18452 oduglb 18454 2sqreu 27500 2sqreunn 27501 2sqreult 27502 2sqreultb 27503 2sqreunnlt 27504 2sqreunnltb 27505 uspgredgiedg 29192 uspgriedgedg 29193 usgredg2vlem1 29242 usgredg2vlem2 29243 frcond1 30285 frcond2 30286 n4cyclfrgr 30310 cnlnadjlem3 32088 disjrdx 32604 ply1divalg3 35647 lshpsmreu 39110 reuf1odnf 47119 reuf1od 47120 2reu7 47123 2reu8 47124 2reu8i 47125 2reuimp0 47126 isuspgrim0 47872 isuspgrimlem 47874 |
| Copyright terms: Public domain | W3C validator |