| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > 2rexbidva | Structured version Visualization version GIF version | ||
| Description: Formula-building rule for restricted existential quantifiers (deduction form). (Contributed by NM, 15-Dec-2004.) |
| Ref | Expression |
|---|---|
| 2ralbidva.1 | ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 ↔ 𝜒)) |
| Ref | Expression |
|---|---|
| 2rexbidva | ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 2ralbidva.1 | . . . 4 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → (𝜓 ↔ 𝜒)) | |
| 2 | 1 | anassrs 467 | . . 3 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝜓 ↔ 𝜒)) |
| 3 | 2 | rexbidva 3177 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑦 ∈ 𝐵 𝜒)) |
| 4 | 3 | rexbidva 3177 | 1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∈ wcel 2108 ∃wrex 3070 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-rex 3071 |
| This theorem is referenced by: 2reu4lem 4522 wrdl3s3 15001 bezoutlem2 16577 bezoutlem4 16579 vdwmc2 17017 lsmcom2 19673 lsmass 19687 lsmcomx 19874 lsmspsn 21083 hausdiag 23653 imasf1oxms 24502 mulsval 28135 mulscom 28165 addsdi 28181 mulsasslem3 28191 mulsunif2lem 28195 istrkg2ld 28468 iscgra 28817 axeuclid 28978 elwwlks2 29986 elwspths2spth 29987 fusgr2wsp2nb 30353 shscom 31338 lsmssass 33430 sategoelfvb 35424 3dim0 39459 islpln5 39537 islvol5 39581 isline2 39776 isline3 39778 paddcom 39815 cdlemg2cex 40593 prprspr2 47505 pgrpgt2nabl 48282 elbigolo1 48478 |
| Copyright terms: Public domain | W3C validator |