Theorem vtoclbg 3258

Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 29-Apr-1994.)

Hypotheses

Ref	Expression
vtoclbg.1	⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
vtoclbg.2	⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))
vtoclbg.3	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
vtoclbg	⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃))

Distinct variable groups:   𝑥,𝐴   𝜒,𝑥   𝜃,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)   𝑉(𝑥)

Proof of Theorem vtoclbg

Step	Hyp	Ref	Expression
1		vtoclbg.1	. . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒))
2		vtoclbg.2	. . 3 ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))
3	1, 2	bibi12d 335	. 2 ⊢ (𝑥 = 𝐴 → ((𝜑 ↔ 𝜓) ↔ (𝜒 ↔ 𝜃)))
4		vtoclbg.3	. 2 ⊢ (𝜑 ↔ 𝜓)
5	3, 4	vtoclg 3257	1 ⊢ (𝐴 ∈ 𝑉 → (𝜒 ↔ 𝜃))

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1480   ∈ wcel 1992

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-12 2049  ax-ext 2606

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-v 3193

This theorem is referenced by:  alexeqg  3320  pm13.183  3332  sbc8g  3430  sbc2or  3431  sbcco  3445  sbc5  3447  sbcie2g  3456  eqsbc3  3462  sbcng  3463  sbcimg  3464  sbcan  3465  sbcor  3466  sbcbig  3467  sbcal  3472  sbcex2  3473  sbcel1v  3482  sbcreu  3502  csbiebg  3542  sbcel12  3960  sbceqg  3961  elpwg  4143  snssg  4301  preq12bg  4359  elintgOLD  4454  elintrabg  4459  sbcbr123  4671  opelresg  5367  inisegn0  5460  funfvima3  6450  elixpsn  7892  ixpsnf1o  7893  domeng  7914  1sdom  8108  rankcf  9544  eldm3  31352  br1steqg  31368  br2ndeqg  31369  elima4  31373  brsset  31630  brbigcup  31639  elfix2  31645  elfunsg  31657  elsingles  31659  funpartlem  31683  ellines  31893  elhf2g  31917  cover2g  33127  sbcrexgOLD  36815  sbcangOLD  38207  sbcorgOLD  38208  sbcalgOLD  38220  sbcexgOLD  38221  sbcel12gOLD  38222  sbcel1gvOLD  38563